, A collection of TLA + specifications, 2017.

N. Azmy, S. Merz, C. ;. Weidenbach, T. , V. et al., A rigorous correctness proof for pastry, Abstract State Machines, pp.86-101, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01322342

D. Beyer and M. E. Keremoglu, CPAchecker: A tool for configurable software verification, CAV. pp, pp.184-190, 2011.

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, Symbolic model checking without BDDs, TACAS. LNCS, vol.1579, pp.193-207, 1999.

A. Biere, M. Heule, and H. Van-maaren, Handbook of satisfiability, vol.185, 2009.

G. Bracha and S. Toueg, Asynchronous consensus and broadcast protocols, Journal of the ACM, vol.32, issue.4, pp.824-840, 1985.

T. D. Chandra and S. Toueg, Unreliable failure detectors for reliable distributed systems, Journal of the ACM, vol.43, issue.2, pp.225-267, 1996.

K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz, The TLA + proof system: Building a heterogeneous verification platform, Theoretical aspects of computing, pp.44-44, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00521886

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement for symbolic model checking, J. ACM, vol.50, issue.5, pp.752-794, 2003.

S. Conchon, A. Goel, S. Krstic, A. Mebsout, and F. Za¨?diza¨?di, Cubicle: A parallel smt-based model checker for parameterized systems-tool paper, CAV. pp, pp.718-724, 2012.

E. W. Dijkstra, W. H. Feijen, and A. M. Van-gasteren, Derivation of a termination detection algorithm for distributed computations, Control Flow and Data Flow: concepts of distributed programming, pp.507-512, 1986.

E. Gafni and L. Lamport, Disk paxos, Distributed Computing, vol.16, issue.1, pp.1-20, 2003.

R. Guerraoui, On the hardness of failure-sensitive agreement problems, Information Processing Letters, vol.79, issue.2, pp.99-104, 2001.

I. Konnov, M. Lazi´clazi´c, H. Veith, and J. Widder, A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms, POPL. pp, pp.719-734, 2017.

D. Kroening and M. Tautschnig, CBMC-C bounded model checker-(competition contribution), TACAS. pp, pp.389-391, 2014.

J. Kukovec, T. H. Tran, and I. Konnov, Extracting symbolic transitions from TLA + specifications (technical report, 2018.

L. Lamport, The part-time parliament, ACM TCS, vol.16, issue.2, pp.133-169, 1998.

L. Lamport, Specifying systems: the TLA + language and tools for hardware and software engineers, 2002.

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

S. Merz and H. Vanzetto, Automatic verification of TLA + proof obligations with SMT solvers, LPAR, vol.7180, pp.289-303, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00760570

S. Merz and H. Vanzetto, Harnessing SMT solvers for TLA+ proofs, ECEASST, vol.53, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00760579

I. Moraru, D. G. Andersen, and M. Kaminsky, There is more consensus in egalitarian parliaments, SOSP. pp, pp.358-372, 2013.

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

D. Ongaro, Consensus: Bridging theory and practice, 2014.

M. Raynal, A case study of agreement problems in distributed systems: Non-blocking atomic commitment, pp.209-214, 1997.

Y. Yu, P. Manolios, and L. Lamport, Model checking TLA + specifications, Correct Hardware Design and Verification Methods, pp.54-66, 1999.