A. Miné, Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations, Proc. of the 4th Int. Workshop on Numerical and Symbolic Abstract Domains (NSAD'12), pp.2012-89
DOI : 10.1016/j.entcs.2012.09.009

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

J. Brauer and A. Simon, Inferring Definite Counterexamples through Under-Approximation, Lect. Notes Comput. Sci, vol.7226, pp.54-69, 2012.
DOI : 10.1007/978-3-642-28891-3_7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.385.1908

C. Popeea, D. N. Xu, and W. Chin, A practical and precise inference and specializer for array bound checks elimination, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation , PEPM '08, pp.177-187, 2008.
DOI : 10.1145/1328408.1328434

D. Massé, Temporal property-driven verification by abstract interpretation, 2002.

E. W. 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

J. Morris, Non-deterministic expressions and predicate transformers, Information Processing Letters, vol.61, issue.5, pp.241-246, 1997.
DOI : 10.1016/S0020-0190(97)00023-9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.3073

J. Filliâtre, Deductive software verification, International Journal on Software Tools for Technology Transfer, vol.21, issue.2, pp.397-403, 2011.
DOI : 10.1007/s10009-011-0211-0

E. A. Emerson, The beginning of model checking: A personal perspective, in: 25 Years of Model Checking, pp.27-45, 2008.

A. Armando, J. Mantovani, and L. Platania, Bounded model checking of software using SMT solvers instead of SAT solvers, International Journal on Software Tools for Technology Transfer, vol.31, issue.1, pp.69-83, 2009.
DOI : 10.1007/s10009-008-0091-0

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM, vol.50, issue.5, pp.752-794, 2003.
DOI : 10.1145/876638.876643

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, 1978.

J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., Static analysis and verification of aerospace software by abstract interpretation, pp.2010-3385, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00528611

P. Cousot and R. Cousot, Static determination of dynamic properties of programs, Proc. of the Second Int. Symp. on Programming, pp.106-130, 1976.

P. Cousot and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78, pp.84-97, 1978.
DOI : 10.1145/512760.512770

A. Miné, The octagon abstract domain, Higher-Order and Symbolic Computation, vol.2477, issue.3, pp.31-100, 2006.
DOI : 10.1007/s10990-006-8609-1

F. Bourdoncle, Abstract debugging of higher-order imperative languages, Proc. of the ACM Conf. on Programing Language Design and Implementation (PLDI'93), pp.46-55, 1993.

D. A. Schmidt, Closed and Logical Relations for Over- and Under-Approximation of Powersets, Proc. of the 11th Int. Symp. on Static Analysis (SAS'04), pp.22-37, 2004.
DOI : 10.1007/978-3-540-27864-1_5

Y. Moy, Sufficient Preconditions for Modular Assertion Checking, Proc. of the 9th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'08), 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

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

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

D. A. Schmidt, Underapproximating Predicate Transformers, Proc. of 13th Int. Symp. on Static Analysis (SAS'06), pp.127-143, 2006.
DOI : 10.1007/11823230_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.68.4693

E. Goubault and S. Putot, Under-Approximations of Computations in Real Numbers Based on Generalized Affine Arithmetic, Proc. of the 14th Int. Symp. on Static Analysis (SAS'07), pp.137-152, 2007.
DOI : 10.1007/978-3-540-74061-2_9

A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, vol.5, issue.2, pp.285-310, 1955.
DOI : 10.2140/pjm.1955.5.285

P. Cousot and R. Cousot, Constructive versions of Tarski???s fixed point theorems, Pacific Journal of Mathematics, vol.82, issue.1, pp.43-57, 1979.
DOI : 10.2140/pjm.1979.82.43

P. Cousot, R. Cousot, and F. Logozzo, Precondition Inference from Intermittent Assertions and Application to Contracts on Collections, Proc. of the 12th Int. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI'11), pp.150-168, 2011.
DOI : 10.1007/11547662_21
URL : https://hal.archives-ouvertes.fr/inria-00543881

P. Cousot and R. Cousot, An abstract interpretation framework for termination, Conf. Rec. of the 39 th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp.245-258

G. Lalire, M. Argoud, and B. Jeannet, Interproc static analyzer, 2011.

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

D. A. Schmidt, Abstract Interpretation From a Denotational-semantics Perspective, Proc. 25th Conf, pp.19-37, 2009.
DOI : 10.1016/j.entcs.2009.07.082

F. Bourdoncle, Efficient chaotic iteration strategies with widenings, Proc. of the Int. Conf. on Formal Methods in Programming and their Applications (FMPA'93), pp.128-141, 1993.
DOI : 10.1007/BFb0039704
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.3357

D. Nguyen-que, Robust and generic abstract domain for static program analysis: the polyhedral case, 2010.

K. Larsen, F. Larsson, P. Pettersson, and W. Yi, Efficient verification of real-time systems: compact data structure and state-space reduction, Proceedings Real-Time Systems Symposium, pp.14-24, 1997.
DOI : 10.1109/REAL.1997.641265

P. Cousot and R. Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, Proc. of the Int. Workshop on Programming Language Implementation and Logic Programming (PLILP'92), pp.269-295, 1992.
DOI : 10.1007/3-540-55844-6_142

R. Bagnara, P. M. Hill, and E. Zaffanella, Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness, Formal Methods in System Design, vol.27, issue.2, pp.279-323, 2009.
DOI : 10.1007/s10703-009-0073-1

A. Miné, Symbolic Methods to Enhance the Precision of Numerical Abstract Domains, Proc. of the 7th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'06), pp.348-363, 2006.
DOI : 10.1007/11609773_23

B. Jeannet and A. Miné, Apron: A Library of Numerical Abstract Domains for Static Analysis, Proc. of the 21th Int. Conf. on Computer Aided Verification (CAV'09), pp.661-667, 2009.
DOI : 10.1007/978-3-642-02658-4_52
URL : https://hal.archives-ouvertes.fr/hal-00786354

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

C. Urban, The Abstract Domain of Segmented Ranking Functions, Proc. of the 20th Int. Symp. on Static Analysis (SAS'13), pp.43-62, 2013.
DOI : 10.1007/978-3-642-38856-9_5
URL : https://hal.archives-ouvertes.fr/hal-00925670

A. Miné, The Banal static analyzer prototype, 2012.

C. Flanagan, R. Leino, M. Lillibridge, G. Nelson, J. Saxe et al., Extended static checking for Java, Proc. of the SIGPLAN Conf. on Programming Language Design and Implementation (PLDI'02), pp.234-245, 2002.