B. Alpern and F. B. Schneider, Defining liveness, Information Processing Letters, vol.21, issue.4, pp.181-185, 1985.
DOI : 10.1016/0020-0190(85)90056-0

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

T. Bouton, D. C. De-oliveira, D. Déharbe, and P. Fontaine, veriT: An Open, Trustable and Efficient SMT-Solver, pp.151-156, 2009.
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634

A. Chaieb and T. Nipkow, Proof Synthesis and Reflection for Linear Arithmetic, Journal of Automated Reasoning, vol.10, issue.5, pp.33-59, 2008.
DOI : 10.1007/s10817-008-9101-x

P. Corbineau, A Declarative Language for the Coq Proof Assistant, Workshop on Types for Proofs and Programs, pp.69-84, 2007.
DOI : 10.1007/978-3-540-68103-8_5

E. Gafni and L. Lamport, Disk Paxos, Distributed Computing, vol.16, issue.1, pp.1-20, 2003.
DOI : 10.1007/s00446-002-0070-8

L. Lamport, Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, vol.3, issue.2, pp.125-143, 1977.
DOI : 10.1109/TSE.1977.229904

L. Lamport, How to Write a Proof, The American Mathematical Monthly, vol.102, issue.7, pp.600-608, 1995.
DOI : 10.2307/2974556

L. Lamport, Specifying Systems, 2003.

L. C. Paulson, Isabelle: A Generic Theorem Prover, 1994.
DOI : 10.1007/BFb0030541

P. Rudnicki, An overview of the Mizar project, Workshop on Types for Proofs and Programs, pp.311-332, 1992.

M. Wenzel, The Isabelle, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01126803