C. Barrett, A. Stump, and C. Tinelli, The SMT-LIB standard : Version 2.0, First official release of Version 2.0 of the SMT-LIB standard, 2010.

C. Barrett, C. Tinelli, and . Cvc3, CVC3, Computer Aided Verification, pp.298-302, 2007.
DOI : 10.1007/978-3-540-73368-3_34

F. Besson, P. Fontaine, and L. Théry, A flexible proof format for SMT: a proposal, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00642544

T. Bouton, D. Caminha, B. De-oliveira, D. Déharbe, and P. Fontaine, veriT: An Open, Trustable and Efficient SMT-Solver, Proc. Conference on Automated Deduction (CADE), pp.151-156, 2009.
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634

L. Mendonça-de-moura and N. Bjørner, Z3: An Efficient SMT Solver, Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

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

P. Fontaine, Techniques for Verification of Concurrent Systems with Invariants, 2004.

Y. Ge, C. Barrett, and C. Tinelli, Solving Quantified Verification Conditions Using Satisfiability Modulo Theories, Automated Deduction ? CADE-21, pp.167-182, 2007.
DOI : 10.1007/978-3-540-73595-3_12

M. Moskal, J. Lopuszanski, and J. R. Kiniry, E-matching for Fun and Profit, Proceedings of the 5th Int'l Workshop on Satisfiability Modulo Theories, pp.19-35, 2007.
DOI : 10.1016/j.entcs.2008.04.078