M. Abadi and L. Lamport, The existence of refinement mappings, Theor. Comput. Sci, vol.82, issue.2, pp.253-284, 1991.

M. Abadi and L. Lamport, Composing specifications, ACM Trans. Program. Lang. Syst, vol.15, issue.1, pp.73-132, 1993.

M. Abadi and L. Lamport, Open systems in TLA, Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, pp.81-90, 1994.

M. Abadi and L. Lamport, Conjoining specifications, ACM Trans. Program. Lang. Syst, vol.17, issue.3, pp.507-534, 1995.

J. , The B-Book: Assigning Programs to Meanings, 1996.

J. , Modeling in Event-B, 2010.

B. Alpern and F. B. Schneider, Defining liveness, Inf. Proc. Letters, vol.21, issue.4, pp.181-185, 1985.

K. R. Apt, Ten years of Hoare's logic: A survey -part 1, ACM Trans. Prog. Lang. and Syst, vol.3, issue.4, pp.431-483, 1981.

P. C. Attie, N. Francez, and O. Grumberg, Fairness and hyperfairness in multi-party interactions, Distributed Computing, vol.6, issue.4, pp.245-254, 1993.

N. Azmy, S. Merz, and C. Weidenbach, A machine-checked correctness proof for Pastry, Sci. Comput. Program, vol.158, pp.64-80, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01768758

R. Back, On correct refinement of programs, J. Comp. and System Sci, vol.23, issue.1, pp.49-68, 1981.

C. Barrett and C. Tinelli, Satisfiability modulo theories, Handbook of Model Checking, pp.305-343, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01095009

W. J. Bolosky, J. R. Douceur, and J. Howell, The Farsite project: a retrospective, Operating Systems Review, vol.41, issue.2, pp.17-26, 2007.

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An extensible automated theorem prover producing checkable proofs, 14th Intl. Conf. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), vol.4790, pp.151-165, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00315920

R. M. Burstall, Program proving as hand simulation with a little induction, Information Processing, pp.308-312, 1974.

S. Chand, Y. A. Liu, and S. D. Stoller, Formal verification of Multi-Paxos for distributed consensus, 21st Intl. Symp. Formal Methods (FM 2016), vol.9995, pp.119-136, 2016.

D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts et al., TLA + proofs, FM 2012: Formal Methods -18th International Symposium, vol.7436, pp.147-154, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00726631

E. W. Dijkstra, A Discipline of Programming, 1976.

D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang, Protocol verification as a hardware design aid, IEEE Intl. Conf. Computer Design: VLSI in Computers and Processors, pp.522-525, 1992.

D. Doligez, J. Kriener, L. Lamport, T. Libal, and S. Merz, Coalescing: Syntactic abstraction for reasoning in first-order modal logics, Automated Reasoning in Quantified Non-Classical Logics, vol.33, pp.1-16, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01063512

U. Engberg, P. Grønning, and L. Lamport, Mechanical verification of concurrent systems with TLA, Computer Aided Verification, Fourth International Workshop, CAV '92, vol.663, pp.44-55, 1992.

R. W. Floyd, Assigning meanings to programs, Proc. Symposium on Applied Mathematics, vol.19, pp.19-32, 1967.

P. Godefroid and P. Wolper, A partial approach to model checking, Inf. Comput, vol.110, issue.2, pp.305-326, 1994.

D. Gries and F. B. Schneider, Avoiding the undefined by underspecification, Computer Science Today, vol.1000, pp.366-373, 1995.

Y. Gurevich, Evolving algebras 1993: Lipari guide, Specification and validation methods, pp.9-36, 1995.

C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno et al., Ironfleet: proving practical distributed systems correct, Proc. 25th Symp. Operating Systems Principles, SOSP 2015, pp.1-17, 2015.

C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno et al., Ironfleet: proving safety and liveness of practical distributed systems, Commun. ACM, vol.60, issue.7, pp.83-92, 2017.

G. J. Holzmann, The SPIN Model Checker, 2003.

J. E. Johnson, D. E. Langworthy, L. Lamport, and F. H. Vogt, Formal specification of a web services protocol, J. Log. Algebr. Program, vol.70, issue.1, pp.34-52, 2007.

R. Joshi, L. Lamport, J. Matthews, S. Tasiran, M. R. Tuttle et al., Checking cache-coherence protocols with TLA + . Formal Methods in System Design, vol.22, pp.125-131, 2003.

F. Kröger, LAR: A logic of algorithmic reasoning, Acta Informatica, vol.8, pp.243-266, 1977.

L. Lamport, Proving the correctness of multiprocess programs, IEEE Trans. Software Eng, vol.3, issue.2, pp.125-143, 1977.

L. Lamport, Time, clocks, and the ordering of events in a distributed system, Commun. ACM, vol.21, issue.7, pp.558-565, 1978.

L. Lamport, A new approach to proving the correctness of multiprocess programs, ACM Trans. Program. Lang. Syst, vol.1, issue.1, pp.84-97, 1979.

L. Lamport, Sometime" is sometimes "not never" -on the temporal logic of programs, Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, pp.174-185, 1980.

L. Lamport, What good is temporal logic?, IFIP Congress, pp.657-668, 1983.

L. Lamport, win and sin: Predicate transformers for concurrency, ACM Trans. Program. Lang. Syst, vol.12, issue.3, pp.396-428, 1990.

L. Lamport, The Temporal Logic of Actions, Research Report, vol.79, 1991.

L. Lamport, Hybrid systems in TLA +, Hybrid Systems, vol.736, pp.77-102

. Springer, , 1992.

L. Lamport, The temporal logic of actions, ACM Trans. Program. Lang. Syst, vol.16, issue.3, pp.872-923, 1994.

L. Lamport, How to write a proof, American Mathematical Monthly, vol.102, issue.7, pp.600-608, 1995.

L. Lamport, Fairness and hyperfairness, Distributed Computing, vol.13, issue.4, pp.239-245, 2000.

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

L. Lamport, The PlusCal algorithm language, Theoretical Aspects of Computing -ICTAC 2009, 6th International Colloquium, vol.5684, pp.36-60, 2009.

L. Lamport, Byzantizing Paxos by refinement, Distributed Computing -25th International Symposium, vol.6950, pp.211-224, 2011.

L. Lamport, The TLA + hyperbook, 2015.

L. Lamport, , 2018.

L. Lamport, The TLA + video course, 2018.

L. Lamport and S. Merz, Auxiliary variables in TLA + . CoRR, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01488617

L. Lamport and L. C. Paulson, Should your specification language be typed, ACM Trans. Program. Lang. Syst, vol.21, issue.3, pp.502-526, 1999.

L. Lamport, R. E. Shostak, and M. C. Pease, The byzantine generals problem, ACM Trans. Program. Lang. Syst, vol.4, issue.3, pp.382-401, 1982.

K. R. Leino, Dafny: An automatic program verifier for functional correctness, 16th Intl. Conf. Logic for Programming, vol.6355, pp.348-370, 2010.

O. Lichtenstein and A. Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proc. Twelfth Ann. ACM Symp. Princ. Prog. Lang. (POPL 1985), pp.97-107, 1985.

K. Mcmillan, Symbolic Model Checking, 1993.

S. Merz, A more complete TLA, FM'99: World Congress on Formal Methods, vol.1709, pp.1226-1244, 1999.

S. Merz, The specification language TLA +, Logics of Specification Languages, pp.401-451, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00338330

C. Morgan, Programming from specifications, 1990.

C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker et al., How Amazon Web Services uses formal methods, CACM, vol.58, issue.4, pp.66-73, 2015.

S. S. Owicki and L. Lamport, Proving liveness properties of concurrent programs, ACM Trans. Program. Lang. Syst, vol.4, issue.3, pp.455-495, 1982.

L. C. Paulson, Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol.828, 1994.

A. Pnueli, The temporal logic of programs, Proc. 18th Annual Symposium on the Foundations of Computer Science, pp.46-57, 1977.

A. N. Prior, Past, Present and Future, 1967.

R. L. Schwartz, P. M. Melliar-smith, and F. H. Vogt, An interval-based temporal logic, Proc. Logics of Programs, vol.164, pp.443-457, 1984.

J. M. Spivey, The Z Notation: A reference manual. International Series in Computer Science, 1992.

M. Suda and C. Weidenbach, A PLTL-prover based on labelled superposition with partial model guidance, 6th Intl. Joint Conf. Automated Reasoning (IJCAR 2012, vol.7364, pp.537-543, 2012.

A. Valmari, A stubborn attack on state explosion, 2nd Intl. Wsh. Computer Aided Verification, vol.531, pp.156-165, 1990.