M. Balser, W. Reif, G. Schellhorn, K. Stenzel, and A. Thums, Formal System Development with KIV, LNCS, vol.1783, pp.363-366, 2000.
DOI : 10.1007/3-540-46428-X_25
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.6551

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, LNCS, vol.4790, 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, LNCS, vol.6173, pp.142-148, 2010.
DOI : 10.1007/978-3-642-14203-1_12
URL : https://hal.archives-ouvertes.fr/inria-00534821

L. Lamport, What good is temporal logic?, Information Processing 83, pp.657-668, 1983.

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

L. Lamport, The PlusCal Algorithm Language, LNCS, vol.5684, pp.36-60, 2009.
DOI : 10.1007/978-3-642-03466-4_2

L. Lamport, Byzantizing Paxos by refinement Available at http://research. microsoft.com/en-us/um, 2011.
DOI : 10.1007/978-3-642-24100-0_22

L. Lamport, How to write a 21st century proof, Journal of Fixed Point Theory and Applications, vol.16, issue.5, pp.10-1007, 2012.
DOI : 10.1007/s11784-012-0071-6

T. Lu, S. Merz, and C. Weidenbach, Towards Verification of the Pastry Protocol Using TLA???+???, LNCS, vol.181, pp.244-258, 2011.
DOI : 10.1007/3-540-48153-2_6
URL : https://hal.archives-ouvertes.fr/inria-00593523

S. Merz and H. Vanzetto, Automatic Verification of TLA???+??? Proof Obligations with SMT Solvers, LNCS, vol.7180, pp.289-303, 2012.
DOI : 10.1007/978-3-642-28717-6_23
URL : https://hal.archives-ouvertes.fr/hal-00760570

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, pp.379-394, 2011.
DOI : 10.1109/SP.2011.38
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.206.5025

G. L. Peterson, Myths about the mutual exclusion problem, Information Processing Letters, vol.12, issue.3, pp.115-116, 1981.
DOI : 10.1016/0020-0190(81)90106-X

T. The and . Project, Web page

M. Wenzel, L. C. Paulson, and T. Nipkow, The Isabelle Framework, TPHOLs, pp.33-38, 2008.
DOI : 10.1007/978-3-540-74591-4_26