K. Arnout and B. Meyer, Cover feature - Uncovering hidden contracts: the .net example, Computer, vol.36, issue.11, pp.48-55, 2003.
DOI : 10.1109/MC.2003.1244535

C. Baier and J. P. Katoen, Principles of Model Checking, 2008.

M. Barnett, M. Fähndrich, D. Garbervetsky, and F. Logozzo, Annotations for (more) precise points-to analysis. IWACO '07, 2007.

M. Barnett, M. Fähndrich, and F. Logozzo, Embedded contract languages. SAC'10, pp.2103-2110, 2010.

A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zhu, Bounded Model Checking, Advances in Computers, vol.58, pp.118-149, 2003.
DOI : 10.1016/S0065-2458(03)58003-2

F. Bourdoncle, Abstract debugging of higher-order imperative languages. PLDI '93, pp.46-55, 1993.

C. Calcagno, D. Distefano, P. O-'hearn, and H. Yang, Compositional shape analysis by means of bi-abduction. 36 th POPL, pp.289-300, 2009.

S. Chandra, S. Fink, and M. Sridharan, Snugglebug: a powerful approach to weakest preconditions. PLDI, pp.363-374, 2009.

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, Thèse d' ´ EtatèsEtatès sciences mathématiques, 1978.

P. Cousot, Semantic foundations of program analysis Program Flow Analysis: Theory and Applications, ch, pp.303-342, 1981.

P. Cousot, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Theoretical Computer Science, vol.277, issue.1-2, pp.47-103, 2002.
DOI : 10.1016/S0304-3975(00)00313-3

P. Cousot and R. Cousot, Static determination of dynamic properties of recursive procedures, IFIP Conf. on Formal Description of Programming Concepts, pp.237-277, 1977.

P. Cousot and R. Cousot, Systematic design of program analysis frameworks. 6 th POPL, pp.269-282, 1979.

P. Cousot and R. Cousot, Abstract interpretation and application to logic programs, The Journal of Logic Programming, vol.13, issue.2-3, pp.103-179, 1992.
DOI : 10.1016/0743-1066(92)90030-7
URL : http://doi.org/10.1016/0743-1066(92)90030-7

P. Cousot and R. Cousot, Modular static program analysis. CC, LNCS, vol.2304, pp.159-178, 2002.
DOI : 10.1007/3-540-45937-5_13
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.139.6522

P. Cousot, R. Cousot, and F. Logozzo, A parametric segmentation functor for fully automatic and scalable array content analysis, 2011.
DOI : 10.1145/1925844.1926399
URL : https://hal.archives-ouvertes.fr/inria-00543874

E. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, vol.18, issue.8, pp.453-457, 1975.
DOI : 10.1145/360933.360975

M. Fähndrich and F. Logozzo, Clousot: Static contract checking with abstract interpretation. FoVeOOS, 2010.

S. Gulwani and A. Tiwari, Computing Procedure Summaries for Interprocedural Analysis, LNCS, vol.07, issue.4421, pp.253-267, 2007.
DOI : 10.1007/978-3-540-71316-6_18
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.224.1235

M. Hecht, Flow Analysis of Computer Programs, 1977.

J. King, Symbolic execution and program testing, Communications of the ACM, vol.19, issue.7, pp.385-394, 1976.
DOI : 10.1145/360248.360252

B. Meyer, Eiffel: The Language, 1991.

B. Meyer, Applying 'design by contract', Computer, vol.25, issue.10, pp.40-51, 1992.
DOI : 10.1109/2.161279
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.72.7831

Y. Moy, Sufficient preconditions for modular assertion checking. VMCAI 08, LNCS, vol.4905, pp.188-202, 2008.
DOI : 10.1007/978-3-540-78163-9_18
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.101.6082

D. Park, Fixpoint induction and proofs of program properties, Machine Intelligences, pp.59-78, 1969.

X. Rival, Understanding the Origin of Alarms in Astr??e, SAS '05, 303?319, 2005.
DOI : 10.1007/11547662_21

T. Lev-ami, M. Sagiv, T. Reps, and S. Gulwani, Backward analysis for inferring quantified preconditions, 2007.