, A collection of TLA + specifications, 2017.
A rigorous correctness proof for pastry, Abstract State Machines, pp.86-101, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01322342
CPAchecker: A tool for configurable software verification, CAV. pp, pp.184-190, 2011. ,
Symbolic model checking without BDDs, TACAS. LNCS, vol.1579, pp.193-207, 1999. ,
, Handbook of satisfiability, vol.185, 2009.
Asynchronous consensus and broadcast protocols, Journal of the ACM, vol.32, issue.4, pp.824-840, 1985. ,
Unreliable failure detectors for reliable distributed systems, Journal of the ACM, vol.43, issue.2, pp.225-267, 1996. ,
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
Counterexample-guided abstraction refinement for symbolic model checking, J. ACM, vol.50, issue.5, pp.752-794, 2003. ,
Cubicle: A parallel smt-based model checker for parameterized systems-tool paper, CAV. pp, pp.718-724, 2012. ,
Derivation of a termination detection algorithm for distributed computations, Control Flow and Data Flow: concepts of distributed programming, pp.507-512, 1986. ,
Disk paxos, Distributed Computing, vol.16, issue.1, pp.1-20, 2003. ,
On the hardness of failure-sensitive agreement problems, Information Processing Letters, vol.79, issue.2, pp.99-104, 2001. ,
A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms, POPL. pp, pp.719-734, 2017. ,
CBMC-C bounded model checker-(competition contribution), TACAS. pp, pp.389-391, 2014. ,
Extracting symbolic transitions from TLA + specifications (technical report, 2018. ,
The part-time parliament, ACM TCS, vol.16, issue.2, pp.133-169, 1998. ,
Specifying systems: the TLA + language and tools for hardware and software engineers, 2002. ,
The specification language TLA +, Logics of specification languages, pp.401-451, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00338330
Automatic verification of TLA + proof obligations with SMT solvers, LPAR, vol.7180, pp.289-303, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00760570
Harnessing SMT solvers for TLA+ proofs, ECEASST, vol.53, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00760579
There is more consensus in egalitarian parliaments, SOSP. pp, pp.358-372, 2013. ,
How Amazon web services uses formal methods, Comm. ACM, vol.58, issue.4, pp.66-73, 2015. ,
Consensus: Bridging theory and practice, 2014. ,
A case study of agreement problems in distributed systems: Non-blocking atomic commitment, pp.209-214, 1997. ,
Model checking TLA + specifications, Correct Hardware Design and Verification Methods, pp.54-66, 1999. ,