C. Barrett, A. Stump, and C. Tinelli, The SMT-LIB standard: Version 2.0, Satisfiability Modulo Theories, 2010.

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, 23rd Intl. Conf. Automated Deduction, pp.116-130, 2011.
DOI : 10.1007/BFb0028402
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.194.1769

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, 14th Intl. Conf. Logic for Programming, pp.151-165, 2007.
DOI : 10.1007/978-3-540-75560-9_13
URL : https://hal.archives-ouvertes.fr/inria-00315920

K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz, Verifying Safety Properties with the TLA???+??? Proof System
DOI : 10.1007/978-3-642-14203-1_12
URL : https://hal.archives-ouvertes.fr/inria-00534821

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

D. Déharbe, Automatic verification for a class of proof obligations with SMTsolvers, Abstract State Machines, pp.217-230, 2010.

B. Dutertre and L. De-moura, The Yices SMT solver, 2006.

L. Lamport, A new solution of Dijkstra's concurrent programming problem, Communications of the ACM, vol.17, issue.8, pp.453-454, 1974.
DOI : 10.1145/361082.361093

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

L. Lamport and L. C. Paulson, Should your specification language be typed, ACM Transactions on Programming Languages and Systems, vol.21, issue.3, pp.502-526, 1999.
DOI : 10.1145/319301.319317
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.2302

B. Parno, J. R. Lorch, J. R. Douceur, J. Mickens, and J. M. Mccune, Memoir: Practical State Continuity for Protected Modules, 2011 IEEE Symposium on Security and Privacy, 2011.
DOI : 10.1109/SP.2011.38
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.206.5025

M. Wenzel, L. C. Paulson, and T. Nipkow, The Isabelle Framework, 21st Intl. Conf. Theorem Proving in Higher Order Logics, pp.33-38, 2008.
DOI : 10.1007/978-3-540-74591-4_26