Definability of Accelerated Relations in a Theory of Arrays and Its Applications, Symposium on Frontiers of Combining Systems (FCS), pp.23-39 ,
DOI : 10.1007/978-3-642-40885-4_3
Decision procedures for flat array properties, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.15-30, 2014. ,
Invariant Synthesis for Combined Theories, Verification, Model Checking, and Abstract Interpretation (VMCAI), pp.378-394, 2007. ,
DOI : 10.1007/978-3-540-69738-1_27
A static analyzer for large safety-critical software, ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp.196-207, 2003. ,
URL : https://hal.archives-ouvertes.fr/hal-00128135
What???s Decidable About Arrays?, Verification, Model Checking, and Abstract Interpretation (VMCAI), pp.427-442, 2006. ,
DOI : 10.1007/11609773_28
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.119.4969
Relational inductive shape analysis, ACM Symposium on Principles of Programming Languages (POPL), pp.247-260, 2008. ,
Modular construction of shape-numeric analyzers, Semantics, Abstract Interpretation, and Reasoning about Programs (SAIRP), pp.161-185, 2013. ,
Shape analysis with structural invariant checkers, Static Analysis Symposium (SAS), pp.384-401, 2007. ,
A Sound Floating-Point Polyhedra Abstract Domain, Asian Symposium on Programming Languages and Systems (APLAS), pp.3-18, 2008. ,
DOI : 10.1007/3-540-45013-0_7
URL : https://hal.archives-ouvertes.fr/hal-00531567
Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977. ,
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/hal-01108790
Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '79, pp.269-282, 1979. ,
DOI : 10.1145/567752.567778
A parametric segmentation functor for fully automatic and scalable array content analysis, ACM Symposium on Principles of Programming Languages (POPL), pp.105-118, 2011. ,
URL : https://hal.archives-ouvertes.fr/inria-00543874
Automatic Analysis of Open Objects in Dynamic Language Programs, Static Analysis Symposium (SAS), pp.134-150, 2014. ,
DOI : 10.1007/978-3-319-10936-7_9
URL : https://hal.archives-ouvertes.fr/hal-01095955
QUIC Graphs: Relational Invariant Generation for Containers, European Conference on Object-Oriented Programming (ECOOP), pp.401-425, 2013. ,
DOI : 10.1007/978-3-642-39038-8_17
Fluid Updates: Beyond Strong vs. Weak Updates, European Symposium on Programming (ESOP), pp.246-266, 2010. ,
DOI : 10.1007/978-3-642-11957-6_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.157.7323
Precise reasoning for programs using containers, ACM Symposium on Principles of Programming Languages (POPL), pp.187-200, 2011. ,
DOI : 10.1145/1925844.1926407
Numeric Domains with Summarized Dimensions, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.512-529, 2004. ,
DOI : 10.1007/978-3-540-24730-2_38
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.8931
A framework for numeric analysis of array operations, ACM Symposium on Principles of Programming Languages (POPL), pp.338-350, 2005. ,
Lifting abstract interpreters to quantified logical domains, ACM Symposium on Principles of Programming Languages (POPL), pp.235-246, 2008. ,
DOI : 10.1145/1328438.1328468
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.133.9559
Discovering properties about arrays in simple programs, ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp.339-348, 2008. ,
DOI : 10.1145/1375581.1375623
URL : https://hal.archives-ouvertes.fr/hal-00288274
Apron: A Library of Numerical Abstract Domains for Static Analysis, Computer Aided Verification (CAV), pp.661-667, 2009. ,
DOI : 10.1007/978-3-642-02658-4_52
URL : https://hal.archives-ouvertes.fr/hal-00786354
Array Abstractions from Proofs, Computer Aided Verification (CAV), pp.193-206, 2007. ,
DOI : 10.1007/978-3-540-73368-3_23
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.8283
Finding loop invariants for programs over array using a theorem prover, Fundamental Approaches to Software Engineering (FASE), pp.470-485, 2009. ,
Abstraction of Arrays Based on Non Contiguous Partitions, Verification, Model Checking, and Abstract Interpretation (VMCAI), pp.282-299, 2015. ,
DOI : 10.1007/978-3-662-46081-8_16
URL : https://hal.archives-ouvertes.fr/hal-01095985
Quantified invariant generation using an interpolation saturation prover, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.413-427, 2008. ,
The octagon abstract domain. Higher-Order and Symbolic Computation, pp.31-100, 2006. ,
Faults in linux: ten years later, Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp.305-318, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00940355
Outline of a mathematical theory of computation, 1970. ,
Abstraction refinement for quantified array assertions, Static Analysis Symposium (SAS), pp.3-18, 2009. ,
Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks, Asian Symposium on Programming Languages and Systems (APLAS), pp.131-147, 2012. ,
DOI : 10.1007/978-3-642-35182-2_10
URL : https://hal.archives-ouvertes.fr/hal-00760427
Operating systems: design and implementation, 1987. ,
Reduced Product Combination of Abstract Domains for Shapes, Verification, Model Checking, and Abstract Interpretation (VMCAI), pp.375-395, 2013. ,
DOI : 10.1007/978-3-642-35873-9_23
URL : https://hal.archives-ouvertes.fr/hal-00760428
Scalable Shape Analysis for Systems Code, Computer Aided Verification (CAV), pp.385-398, 2008. ,
DOI : 10.1007/978-3-540-70545-1_36