F. Alberti, S. Ghilardi, and N. Sharygina, 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

F. Alberti, S. Ghilardi, and N. Sharygina, Decision procedures for flat array properties, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.15-30, 2014.

D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko, 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

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., 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

A. R. Bradley, Z. Manna, and H. B. Sipma, 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

. Bor-yuh-evan, X. Chang, and . Rival, Relational inductive shape analysis, ACM Symposium on Principles of Programming Languages (POPL), pp.247-260, 2008.

. Bor-yuh-evan, X. Chang, and . Rival, Modular construction of shape-numeric analyzers, Semantics, Abstract Interpretation, and Reasoning about Programs (SAIRP), pp.161-185, 2013.

X. Bor-yuh-evan-chang, G. C. Rival, and . Necula, Shape analysis with structural invariant checkers, Static Analysis Symposium (SAS), pp.384-401, 2007.

L. Chen, A. Miné, and P. Cousot, 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

P. Cousot and R. Cousot, 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

P. Cousot and R. Cousot, 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

P. Cousot, R. Cousot, and F. Logozzo, 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

A. Cox, . Bor-yuh-evan, X. Chang, and . Rival, 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

A. Cox, . Bor-yuh-evan, S. Chang, and . Sankaranarayanan, 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

I. Dillig, T. Dillig, and A. Aiken, 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

I. Dillig, T. Dillig, and A. Aiken, Precise reasoning for programs using containers, ACM Symposium on Principles of Programming Languages (POPL), pp.187-200, 2011.
DOI : 10.1145/1925844.1926407

D. Gopan, F. Dimaio, N. Dor, T. W. Reps, and S. Sagiv, 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

D. Gopan, T. W. Reps, and S. Sagiv, A framework for numeric analysis of array operations, ACM Symposium on Principles of Programming Languages (POPL), pp.338-350, 2005.

S. Gulwani, B. Mccloskey, and A. Tiwari, 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

N. Halbwachs and M. Péron, 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

B. Jeannet and A. Miné, 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

R. Jhala and K. L. Mcmillan, 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

L. Kovács and A. Voronkov, Finding loop invariants for programs over array using a theorem prover, Fundamental Approaches to Software Engineering (FASE), pp.470-485, 2009.

J. Liu and X. Rival, 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

L. Kenneth and . Mcmillan, Quantified invariant generation using an interpolation saturation prover, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.413-427, 2008.

A. Miné, The octagon abstract domain. Higher-Order and Symbolic Computation, pp.31-100, 2006.

N. Palix, G. Thomas, S. Saha, C. Calvès, J. L. Lawall et al., 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

D. Scott, Outline of a mathematical theory of computation, 1970.

M. Nassim-seghir, A. Podelski, and T. Wies, Abstraction refinement for quantified array assertions, Static Analysis Symposium (SAS), pp.3-18, 2009.

P. Sotin and X. Rival, 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

S. Andrew, . Tanenbaum, S. Albert, . Woodhull, S. Andrew et al., Operating systems: design and implementation, 1987.

A. Toubhans, . Bor-yuh-evan, X. Chang, and . Rival, 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

H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook et al., Scalable Shape Analysis for Systems Code, Computer Aided Verification (CAV), pp.385-398, 2008.
DOI : 10.1007/978-3-540-70545-1_36