D. Cansell and D. Méry, Foundations of the B method, Computing and Informatics, pp.1-31, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099794

A. Chaieb, Mechanized quantifier elimination for linear real-arithmetic in Isabelle, 2006.

D. Déharbe, P. Fontaine, and S. Ranise, The haRVey theorem prover

P. Fontaine, Techniques for verification of concurrent systems with invariants, 2004.

P. Fontaine, J. Marion, S. Merz, L. P. Nieto, and A. Tiu, Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, TACAS 2006, pp.167-181, 2006.
DOI : 10.1007/3-540-45620-1_26
URL : https://hal.archives-ouvertes.fr/inria-00001088

J. Harrison, Metatheory and reflection in theorem proving: A survey and critique, 1995.

J. R. Kiniry, D. R. Cok, and . Esc, Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2 and a report on a case study involving the use of ESC/Java2 to verify portions of an Internet voting tally system, CASSIS'2004, pp.108-128, 2005.

L. Lamport, The book Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, 2002.

D. Loveland, Automated theorem proving: A logical basis, Fundamental studies in Computer Science, 1978.

T. Nipkow, G. Bauer, and P. Schultz, Flyspeck I: Tame Graphs, Automated Reasoning, 2006.
DOI : 10.1007/11814771_4

T. Nipkow, L. Paulson, M. Wenzel, /. Isabelle, and . Hol, A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science, 2002.

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, Lecture Notes in Artificial Intelligence, vol.607, pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217

S. Ranise and C. Tinelli, The smt-lib standard: Version 1.1, 2005.

T. Weber, Integrating a SAT Solver with an LCF-style Theorem Prover, PDPAR'05, 2005.
DOI : 10.1016/j.entcs.2005.12.007