T. Ball, A. Podelski, and S. K. Rajamani, Relative Completeness of Abstraction Refinement for Software Model Checking, Proc. 8 th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, pp.158-172, 2002.
DOI : 10.1007/3-540-46002-0_12

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

D. Boucher and M. Feeley, Abstract compilation: A new implementation paradigm for static analysis, Proc. 6th Int. Conf. on Compiler Construction, CC '96, pp.192-207, 1996.
DOI : 10.1007/3-540-61053-7_62

A. R. Bradley and Z. Manna, The Calculus of Computation, Decision procedures with Applications to Verification, 2007.

R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.677-691, 1986.
DOI : 10.1109/TC.1986.1676819

C. C. Chang and H. J. Keisler, Model theory. volume 73 of Studies in logic and the foundation of mathematics, 1990.

E. M. Clarke, A. Biere, R. Raimi, and Y. Zhu, Bounded model checking using satisfiability solving, Formal Methods in System Design, vol.19, issue.1, pp.7-34, 2001.
DOI : 10.1023/A:1011276507260

E. M. Clarke, O. Grumberg, and D. A. , Peled. Model Checking, 1999.

M. Codish and H. Søndergaard, Meta-circular abstract interpretation in Prolog The Essence of Computation: Complexity, Analysis, Transformation, LNCS, vol.2566, pp.109-134, 2002.

S. A. Cook, Soundness and Completeness of an Axiom System for Program Verification, SIAM Journal on Computing, vol.7, issue.1, pp.70-80, 1978.
DOI : 10.1137/0207005

D. C. Cooper, Theorem proving in arithmetic without multiplication, Machine Intelligence, vol.91, issue.7, pp.91-99, 1972.

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

P. Cousot, Methods and logics for proving programs Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science, chapter 15, pp.843-993, 1990.

P. Cousot, Verification by Abstract Interpretation, Proc. 23rd Int. Col., ICALP '96, pp.1-3, 1996.
DOI : 10.1007/978-3-540-39910-0_11

URL : https://hal.archives-ouvertes.fr/inria-00528611

P. Cousot, Abstract interpretation based static analysis parameterized by semantics, Pro. 4th Int. Symp. on Static Analysis, SAS '97, pp.388-394, 1997.
DOI : 10.1007/BFb0032759

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 programs, Proc. 2 nd Int. Symp. on Programming, pp.106-130, 1976.

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, 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 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 and R. Cousot, Abstract Interpretation Frameworks, Journal of Logic and Computation, vol.2, issue.4, pp.511-547, 1992.
DOI : 10.1093/logcom/2.4.511

P. Cousot and R. Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, Proc. 4 th Int. Symp. Programming Language Implementation and Logic Programming, PLILP '92, pp.26-28, 1992.
DOI : 10.1007/3-540-55844-6_142

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The Astrée analyser, Proc. 14 th European Symp. on Programming Languages and Systems, pp.21-30, 2005.

L. De-moura, H. Rueß, and M. Sorea, Bounded Model Checking and Induction: From Refutation to Verification, Proc. 15th Computer-Aided Verification conf. (CAV'03), volume 2725 of LNCS, pp.14-26, 2003.
DOI : 10.1007/978-3-540-45069-6_2

D. Detlefs, G. Nelson, and J. B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005.
DOI : 10.1145/1066100.1066102

A. Ehrenfeucht, Decidability of the theory of one function. Notices Amer, Math. Soc, vol.6, p.268, 1959.

J. Ferrante and J. R. Geiser, An efficient decision procedure for the theory of rational order, Theoretical Computer Science, vol.4, issue.2, pp.227-233, 1977.
DOI : 10.1016/0304-3975(77)90037-8

J. Ferrante and C. Rackoff, A Decision Procedure for the First Order Theory of Real Addition with Order, SIAM Journal on Computing, vol.4, issue.1, pp.69-76, 1975.
DOI : 10.1137/0204006

R. W. Floyd, Assigning meaning to programs, Pro. Symp. in Applied Mathematics, pp.19-32, 1967.

Y. Ge, C. Barrett, and C. Tinelli, Solving quantified verification conditions using satisfiability modulo theories. Conf. on Automated Deduction, pp.4603-167, 2007.

Y. Ge and L. De-moura, Complete instantiation of quantified formulas in satisfiability modulo theories, LNCS, vol.5643, pp.306-320, 2009.

S. Gulwani, B. Mccloskey, and A. Tiwari, Lifting abstract interpreters to quantified logical domains, 35 th POPL, pp.235-246, 2008.

S. Gulwani and A. Tiwari, Combining abstract interpreters, PLDI 2006, pp.376-386, 2006.

P. Hitchcock and D. Park, Induction rules and termination proofs, Proc. 1st Int. Colloq. on Automata, Languages and Programming, pp.225-251, 1973.

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259

J. C. King, A Program Verifier, 1969.

D. C. Luckham, D. M. Park, and M. S. Paterson, On formalised computer programs, Journal of Computer and System Sciences, vol.4, issue.3, pp.220-240, 1970.
DOI : 10.1016/S0022-0000(70)80022-8

L. Mauborgne, Abstract interpretation using typed decision graphs, Science of Computer Programming, vol.31, issue.1, pp.91-112, 1998.
DOI : 10.1016/S0167-6423(96)00042-1

K. L. Mcmillan, Applying SAT Methods in Unbounded Symbolic Model Checking, Computer Aided Verification, pp.250-264, 2002.
DOI : 10.1007/3-540-45657-0_19

P. Naur, Proof of algorithms by general snapshots, BIT, vol.1, issue.4, pp.310-316, 1966.
DOI : 10.1007/BF01966091

G. Nelson and D. C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257
DOI : 10.1145/357073.357079

V. R. Pratt, Two easy theories whose combination is hard

T. W. Reps, S. Sagiv, and G. Yorsh, Symbolic Implementation of the Best Transformer, Proc. 5 th Int. Conf. on Verification, Model Checking and Abstract Interpretation, pp.252-266, 2004.
DOI : 10.1007/978-3-540-24622-0_21

X. Rival and L. Mauborgne, The trace partitioning abstract domain, ACM Transactions on Programming Languages and Systems, vol.29, issue.5, 2007.
DOI : 10.1145/1275497.1275501

M. Sagiv, T. Reps, and R. Wilhelm, Parametric shape analysis via 3-valued logic, 26 th POPL, pp.238-252, 1999.

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