F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Why3: Shepherd your herd of provers, Boogie 2011: First International Workshop on Intermediate Verification Languages, pp.53-64, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

. Bor-yuh-evan, K. Chang, M. Rustan, and . Leino, Abstract interpretation with alien expressions and heap structures, International Workshop on Verification, Model Checking, and Abstract Interpretation, pp.147-163, 2005.

M. Clochard, L. Gondelman, and M. Pereira, The Matrix Reproved (Verification Pearl), VSTTE 2016, 2016.
DOI : 10.1007/978-3-319-48869-1_8
URL : https://hal.archives-ouvertes.fr/hal-01617437

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-00930103

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

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, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The ASTRE?? Analyzer, European Symposium on Programming, pp.21-30, 2005.
DOI : 10.1007/978-3-540-31987-0_3

B. Dutertre, Solving exists/forall problems with yices, 13th International Workshop on Satisfiability Modulo Theories, 2015.

J. Filliâtre, One Logic to Use Them All, Proceedings of the 24th International Conference on Automated Deduction, CADE'13, pp.1-20, 2013.
DOI : 10.1007/978-3-642-38574-2_1

J. Filliâtre, L. Gondelman, and A. Paskevich, A pragmatic type system for deductive verification, 2016.

C. A. Furia and B. Meyer, Inferring Loop Invariants Using Postconditions, pp.277-300, 2010.
DOI : 10.1145/964001.964028
URL : http://www2.inf.ethz.ch/~meyer/publications/proofs/invariant_inference.pdf

G. Gange, J. A. Navas, P. Schachte, H. Søndergaard, J. Peter et al., An Abstract Domain of Uninterpreted Functions, International Conference on Verification, Model Checking, and Abstract Interpretation, pp.85-103, 2016.
DOI : 10.1007/978-3-662-49122-5_4

S. Gulwani, B. Mccloskey, and A. Tiwari, Lifting abstract interpreters to quantified logical domains, ACM SIGPLAN Notices, vol.43, issue.1, pp.235-246, 2008.
DOI : 10.1145/1328897.1328468
URL : http://www.eecs.berkeley.edu/~billm/tr-2007-87.pdf

J. Hatcliff, T. Gary, K. Leavens, M. Rustan, P. Leino et al., Behavioral interface specification languages, ACM Computing Surveys, vol.44, issue.3, p.16, 2012.
DOI : 10.1145/2187671.2187678
URL : http://research.microsoft.com/~leino/papers/krml188.pdf

C. A. and R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259
URL : http://www.utdallas.edu/~kxh060100/cs6371fa07/hoare.pdf

B. Jeannet and A. Miné, Apron: A Library of Numerical Abstract Domains for Static Analysis, International Conference on Computer Aided Verification, pp.661-667, 2009.
DOI : 10.1007/3-540-45013-0_7
URL : https://hal.archives-ouvertes.fr/hal-00786354

L. Mauborgne, Binary Decision Graphs, International Static Analysis Symposium, pp.101-116, 1999.
DOI : 10.1007/3-540-48294-6_7

Y. Moy, Automatic Modular Static Safety Checking for C Programs, 2009.

Y. Moy and C. Marché, The Jessie plugin for Deduction Verification in Frama-C ? Tutorial and Reference Manual, INRIA & LRI, 2011.

O. Padon, N. Immerman, S. Shoham, A. Karbyshev, and M. Sagiv, Decidability of inferring inductive invariants, ACM SIGPLAN Notices, vol.51, issue.1, pp.217-231, 2016.
DOI : 10.1016/j.entcs.2015.02.003

G. Singh, M. Püschel, and M. Vechev, Fast polyhedra abstract domain, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp.46-59, 2017.
DOI : 10.1145/3093333.3009885

N. Suzuki and D. Jefferson, Verification Decidability of Presburger Array Programs, Journal of the ACM, vol.27, issue.1, pp.191-205, 1980.
DOI : 10.1145/322169.322185

G. Winskel, The formal semantics of programming languages: an introduction, 1993.