P. Cousot, Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes

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/inria-00528590

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

M. Sagiv, T. Reps, and R. Wilhelm, Parametric shape analysis via 3-valued logic, POPL'99, 1999.

P. Lam, V. Kuncak, and M. Rinard, Generalized Typestate Checking for Data Structure Consistency, 6th International Conference on Verification, Model Checking and Abstract Interpretation, 2005.
DOI : 10.1007/978-3-540-30579-8_28

J. C. Reynolds, Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp.55-74, 2002.
DOI : 10.1109/LICS.2002.1029817

J. C. Reynolds, Syntactic control of interference, POPL'78, pp.39-46, 1978.

S. Ishtiaq and P. O. Hearn, BI as an assertion language for mutable data structures, POPL'01, pp.14-26, 2001.

H. Yang and P. O. Hearn, A Semantic Basis for Local Reasoning, FoSSaCS'02, pp.402-416, 2002.
DOI : 10.1007/3-540-45931-6_28

´. Sims, Extending separation logic with fixpoints and postponed substitution., in AMAST, Lecture Notes in Computer Science Theoretical Computer Science, vol.311614, issue.351, pp.475-490, 2004.
DOI : 10.1007/978-3-540-27815-3_36
URL : http://dx.doi.org/10.1016/j.tcs.2005.09.071

J. W. De-bakker, Mathematical Theory of Program Correctness, 1980.

H. Y. O-'hearn and J. Reynolds, Syntactic control of interference, POPL'04, Italy, 2004.

H. Y. Lee and K. Yi, Automatic verification of pointer programs using grammarbased shape analysis, ESOP'05, 2005.

A. Miné, A New Numerical Abstract Domain Based on Difference-Bound Matrices, PADO II, pp.155-172, 2001.
DOI : 10.1007/3-540-44978-7_10

C. C. Berdine and P. O. Hearn, Smallfoot: Modular Automatic Assertion Checking with Separation Logic, FMCO'05, 2005.
DOI : 10.1007/11804192_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.63.613

P. O. Distefano and H. Yang, A Local Shape Analysis Based on Separation Logic, TACAS'06, 2006.
DOI : 10.1145/514188.514190

B. C. Berdine and C. Calcagno, Shape Analysis for Composite Data Structures, CAV'07, 2007.
DOI : 10.1007/978-3-540-73368-3_22
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.134.5359

P. O. Calcagno, D. Distefano, and H. Yang, Footprint Analysis: A Shape Analysis That Discovers Preconditions, SAS'07, 2007.
DOI : 10.1007/978-3-540-74061-2_25

T. Lev-ami and M. Sagiv, TVLA: A System for Implementing Static Analyses, SAS'00, 2000.
DOI : 10.1007/978-3-540-45099-3_15

J. Whaley and M. Rinard, Compositional pointer and escape analysis for java programs, Proceedings of the 14th Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications, 1999.
DOI : 10.1145/320385.320400
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.2189

F. Vivien and M. Rinard, Incrementalized pointer and escape analysis, Proceedings of the SIGPLAN '01 Conference on Program Language Design and Implementation, 2001.
DOI : 10.1145/381694.378804
URL : https://hal.archives-ouvertes.fr/hal-00808284

X. R. Chang and G. Necula, Shape Analysis with Structural Invariant Checkers, SAS'07, 2007.
DOI : 10.1007/978-3-540-74061-2_24
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.161.1921

E. C. Magill, A. Nanevski, and P. Lee, Inferring invariants in separation logic for imperative list-processing programs, SPACE'06, 2006.

A. Deutsch, A storeless model of aliasing and its abstractions using finite representations of right-regular equivalence relations, Proceedings of the 1992 International Conference on Computer Languages, 1992.
DOI : 10.1109/ICCL.1992.185463

R. I. Bozga and Y. Lakhnech, Storeless semantics and alias logic, Workshop on Partial Evaluation and Semantics Based Program Manipulation, 2003.
DOI : 10.1145/777388.777395
URL : https://hal.archives-ouvertes.fr/hal-00369341

. Ii, ? T V ar then let vd 01 be such that (v 1 , vd 01 ) ? G 01 ? g 0 to g 0 \ {(x

. Iii, = x then let vd 01 be such that (v 0 , vd 01 ) ? G 01 ? g 0 to g 0 \ {(x

. Iv, if v 0 , v 1 ? T V ar then let vd 0 01 be such that