A. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses Extending Sledgehammer with SMT solvers, 1st Intl. Conf. Certified Programs and Proofs 23rd Intl. Conf. Automated Deduction. LNCS 6803, pp.135-150, 2011.

D. [. Bonichon, D. Delahaye, and . Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, 14th Intl
DOI : 10.1007/978-3-540-75560-9_13
URL : https://hal.archives-ouvertes.fr/inria-00315920

A. [. Barrett, C. Stump, and . Tinelli, The SMT-LIB Standard: Version 2.0, Satisfiability Modulo Theories, pp.151-165, 2007.

D. [. Chaudhuri, L. Doligez, S. Lamport, and . Merz, Verifying Safety Properties with the TLA???+??? Proof System, 5th Intl. Joint Conf. Automated Reasoning, pp.142-148, 2010.
DOI : 10.1007/978-3-642-14203-1_12
URL : https://hal.archives-ouvertes.fr/inria-00534821

E. Springer and U. , msr-inria.inria.fr/ ? doligez/tlaps/. [dB08] L. de Moura, 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.

]. B. Dd06, L. Dutertre, and . De-moura, The Yices SMT Solver, 2006.

P. [. Déharbe, Y. Fontaine, L. Guyot, and . Voisin, SMT Solvers for Rodin, 3rd Intl. Conf. Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012), pp.194-207, 2012.
DOI : 10.1007/978-3-642-30885-7_14

]. L. Lam74 and . Lamport, A New Solution of Dijkstra's Concurrent Programming Problem, Communications of the ACM, vol.17, issue.8, pp.453-454, 1974.

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

]. K. Mcm11 and . Mcmillan, A Proposal for Translating TLA + to SMT, 2011.

C. [. Mentré, J. Marché, M. Filliâtre, and . Asukaa, SMT Solvers for Rodin, 3rd Intl. Conf. Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012), pp.238-251, 2012.

H. [. Merz and . Vanzetto, Automatic Verification of TLA???+??? Proof Obligations with SMT Solvers, 18th Intl. Conf. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18). Lecture Notes in Computer Science 7180, pp.289-303, 2012.
DOI : 10.1007/978-3-642-28717-6_23
URL : https://hal.archives-ouvertes.fr/hal-00760570

. Pld-+-11-]-b, J. R. Parno, J. R. Lorch, J. Douceur, J. M. Mickens et al., Memoir: Practical State Continuity for Protected Modules, IEEE Symp. Security and Privacy Formal Specifications and Correctness Proofs, 2011.