, APALACHE TLA + model checker (development version), 2017.
, ByMC: Byzantine model checker, 2013.
The blockchain consensus layer and BFT, Bulletin of EATCS, vol.3, issue.123, 2017. ,
Asynchronous consensus and broadcast protocols, J. ACM, vol.32, issue.4, pp.824-840, 1985. ,
TLA + proofs, 18th Intl. Symp. Formal Methods (FM 2012), ser, vol.7436, pp.147-154, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00726631
Non-blocking atomic commit in asynchronous distributed systems with failure detectors, Distributed Computing, vol.15, issue.1, pp.17-25, 2002. ,
A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms, pp.719-734, 2017. ,
Who is afraid of Model Checking Distributed Algorithms, 2012, contribution to: CAV Workshop ,
, What you always wanted to know about model checking of fault-tolerant distributed algorithms, PSI 2015, Revised Selected Papers, ser. LNCS, vol.9609, pp.6-21, 2016.
Specifying systems: the TLA + language and tools for hardware and software engineers, 2002. ,
Synthesis of distributed algorithms with parameterized threshold guards, OPODIS, ser. LIPIcs, vol.95, p.20, 2017. ,
How Amazon web services uses formal methods, Comm. ACM, vol.58, issue.4, pp.66-73, 2015. ,
A case study of agreement problems in distributed systems: Non-blocking atomic commitment, pp.209-214, 1997. ,
Bosco: One-step Byzantine asynchronous consensus, DISC, ser. LNCS, vol.5218, pp.438-450, 2008. ,
Simulating authenticated broadcasts to derive simple fault-tolerant algorithms, Dist. Comp, vol.2, pp.80-94, 1987. ,
Model checking TLA + specifications, Correct Hardware Design and Verification Methods, pp.54-66, 1999. ,