J. Abrial, The B-Book, assigning programs to meaning, 1996.

G. Barthe, B. Grégoire, S. Heraud, and S. Zanella-béguelin, Computer-Aided Security Proofs for the Working Cryptographer, Advances in Cryptology CRYPTO 2011, p.7190, 2011.
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01112075

J. C. Blanchette, S. Böhme, A. Popescu, and N. Smallbone, Encoding Monomorphic and Polymorphic Types, Lecture Notes in Computer Science, vol.7795, p.493507, 2013.
DOI : 10.1007/978-3-642-36742-7_34
URL : http://arxiv.org/abs/1609.08916

J. C. Blanchette and A. Paskevich, TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism, 24th International Conference on Automated Deduction (CADE-24), 2013.
DOI : 10.1007/978-3-642-38574-2_29
URL : https://hal.archives-ouvertes.fr/hal-00825086

F. Bobot, S. Conchon, E. Contejean, M. Iguernelala, S. Lescuyer et al., The Alt-Ergo automated theorem prover, 2008.

F. Bobot, S. Conchon, E. Contejean, and S. Lescuyer, Implementing polymorphism in SMT solvers, Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, SMT '08/BPR '08, p.15, 2008.
DOI : 10.1145/1512464.1512466

F. Bobot, J. Filliâtre, C. Marché, G. Melquiond, and A. Paskevich, Preserving user proofs across specication changes, Veried Software: Theories, Tools, Experiments (5th International Conference VSTTE), 2013.
DOI : 10.1007/978-3-642-54108-7_10
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.406.4215

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

F. Bobot and A. Paskevich, Expressing Polymorphic Types in a Many-Sorted Language, Frontiers of Combining Systems, 8th International Symposium, Proceedings, p.87102, 2011.
DOI : 10.1007/978-3-540-78800-3_24
URL : https://hal.archives-ouvertes.fr/inria-00591414

S. Böhme and T. Nipkow, Sledgehammer: Judgement Day, Lecture Notes in Computer Science, vol.6173, p.107121, 2010.
DOI : 10.1007/978-3-642-14203-1_9

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, LPAR, p.151165, 2007.
DOI : 10.1007/978-3-540-75560-9_13
URL : https://hal.archives-ouvertes.fr/inria-00315920

C. Comar, J. Kanig, and Y. Moy, Integrating formal program verication with testing, Proceedings of the Embedded Real Time Software and Systems conference, p.2012, 2012.

J. Couchot and S. Lescuyer, Handling Polymorphism in Automated Deduction, 21th International Conference on Automated Deduction (CADE-21), p.263278, 2007.
DOI : 10.1007/978-3-540-73595-3_18

M. Daumas and G. Melquiond, Certication of bounds on expressions involving rounded operators, Transactions on Mathematical Software, vol.37, issue.1, p.120, 2010.

L. De-moura and N. Bjørner, Z3, an ecient SMT solver, TACAS, p.337340, 2008.

L. De-moura and B. Dutertre, Yices: An SMT Solver

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

J. Filliâtre, Deductive software verication, International Journal on Software Tools for Technology Transfer (STTT), vol.13, issue.5, p.397403, 2011.

J. Filliâtre, Verifying Two Lines of C with Why3: An Exercise in Program Verification, Veried Software: Theories, Tools, Experiments (4th International Conference VSTTE), p.8397, 2012.
DOI : 10.1145/360051.360224

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

J. Hurd, An lcf-style interface between hol and rst-order logic, number 2392 in LNCS, p.134138, 2002.
DOI : 10.1007/3-540-45620-1_10
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.105.1009

B. Jacobs and F. Piessens, The VeriFast program verier, CW Reports, vol.520, 2008.

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock et al., seL4: Formal verication of an OS kernel, Communications of the ACM, vol.53, issue.6, p.107115, 2010.

K. Korovin, iProver ??? An Instantiation-Based Theorem Prover for First-Order Logic (System Description), Proceedings of the 4th International Joint Conference on Automated Reasoning, pp.292-298, 2008.
DOI : 10.1007/978-3-540-71070-7_24

K. Leino and P. P. Rümmer, A polymorphic intermediate verication language: Design and logical encoding, TACAS 2010, p.312327, 2010.

K. R. Leino, Dafny: An Automatic Program Verifier for Functional Correctness, p.348370, 2010.
DOI : 10.1007/978-3-642-17511-4_20

K. R. Leino, Automating Induction with an SMT Solver, Proc. 13th Int. Conf. Verication, Model Checking, and Abstract Interpretation, 2012.
DOI : 10.1007/978-3-540-45085-6_28

X. Leroy, A formally veried compiler back-end, Journal of Automated Reasoning, vol.43, issue.4, p.363446, 2009.

M. Manzano, Extensions of rst order logic, 1996.

C. Marché, C. Paulin-mohring, and X. Urbain, The Krakatoa tool for certication of Java/JavaCard programs annotated in JML, Journal of Logic and Algebraic Programming, vol.58, issue.12, p.89106, 2004.

J. Meng and L. C. Paulson, Translating higher-order clauses to rst-order clauses, Journal of Automated Reasoning, vol.40, p.3560, 2008.
DOI : 10.1007/s10817-007-9085-y
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.64.573

D. Mentré, C. Marché, J. Filliâtre, and M. Asuka, Discharging Proof Obligations from Atelier??B Using Multiple Automated Provers, ABZ'2012 -3rd International Conference on Abstract State Machines, Alloy, pp.238-251, 2012.
DOI : 10.1007/978-3-642-30885-7_17

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, 11th International Conference on Automated Deduction, p.748752, 1992.
DOI : 10.1007/3-540-55602-8_217

W. Reif, G. Schnellhorn, and K. Stenzel, Proving System Correctness with KIV 3.0, 14th International Conference on Automated Deduction, p.6972, 1997.
DOI : 10.1007/3-540-63104-6_10

W. Schulte, S. Xia, J. Smans, and F. Piessens, A glimpse of a verifying C compiler

S. Schulz, System Description: E??0.81, Second International Joint Conference on Automated Reasoning, p.223228, 2004.
DOI : 10.1007/978-3-540-25984-8_15

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., SPASS Version 3.5, 22nd International Conference on Automated Deduction, p.140145, 2009.
DOI : 10.1007/978-3-540-73595-3_38