C. Barrett and C. Tinelli, CVC3, 19 th International Conference on Computer Aided Verification (CAV '07), pp.298-302, 2007.
DOI : 10.1007/978-3-540-73368-3_34

C. Barrett, A. Stump, and C. Tinelli, The SMT-LIB Standard: Version 2.0, 2010.

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, 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

L. 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

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-455, 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

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

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