General decidability theorems for infinite-state systems, LICS, pp.313-321, 1996. ,
Parameterized model checking of synchronous distributed algorithms by abstraction, Verification, Model Checking, and Abstract Interpretation, vol.10747, pp.1-24, 2018. ,
Liveness of parameterized timed networks, ICALP 2015, vol.9135, pp.375-387, 2015. ,
Distributed Computing, 2004. ,
FAST extended release, CAV 2006, vol.4144, pp.63-66, 2006. ,
URL : https://hal.archives-ouvertes.fr/hal-00344195
, CAV 2011, vol.6806, pp.171-177, 2011.
Asymptotically optimal distributed consensus, 1989. ,
, Towards optimal distributed consensus, pp.410-415, 1989.
Synchronous consensus under hybrid process and link failures, Theor. Comput. Sci, vol.412, issue.40, pp.5602-5630, 2011. ,
Symbolic model checking without BDDs, TACAS 1999, vol.1579, pp.193-207 ,
, , 1999.
, Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, 2015.
Tight bounds for k-set agreement, J. ACM, vol.47, issue.5, pp.912-943, 2000. ,
Completeness and complexity of bounded model checking, 2004. ,
, LNCS, vol.2937, pp.85-96, 2004.
A logic-based framework for verifying consensus algorithms, VMCAI 2014, vol.8318, pp.161-181, 2014. ,
Automatic verification of parameterized synchronous systems, CAV 1996, vol.1102, pp.87-98, 1996. ,
On reasoning about rings, Int. J. Found. Comput. Sci, vol.14, issue.4, pp.527-550, 2003. ,
Impossibility of distributed consensus with one faulty process, J. ACM, vol.32, issue.2, pp.374-382, 1985. ,
A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms, pp.719-734, 2017. ,
SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms, CAV 2015, vol.9206, pp.85-102, 2015. ,
On the completeness of bounded model checking for threshold-based distributed algorithms: reachability, Inf. Comput, vol.252, pp.95-109, 2017. ,
Efficient computation of recurrence diameters, VMCAI 2003, vol.2575, pp.298-309, 2003. ,
Reachability in parameterized systems: all flavors of threshold automata, CONCUR, pp, vol.19, p.17, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01871142
Synthesis of distributed algorithms with parameterized threshold guards, OPODIS. LIPIcs, vol.95, p.20, 2017. ,
Flat counter automata almost everywhere!, ATVA 2005, vol.3707, pp.489-503, 2005. ,
URL : https://hal.archives-ouvertes.fr/hal-00346310
Distributed Algorithms, 1996. ,
Cutoff bounds for consensus algorithms, CAV 2017, vol.10427, pp.217-237 ,
, , 2017.
Computation: Finite and Infinite Machines, 1967. ,
Z3: an efficient SMT solver, TACAS 2008, vol.4963, pp.337-340, 2008. ,
Fault-Tolerant Agreement in Synchronous Message-Passing Systems, Synthesis Lectures on Distributed Computing Theory, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00543049
Optimal clock synchronization, J. ACM, vol.34, issue.3, pp.626-645, 1987. ,
Simulating authenticated broadcasts to derive simple faulttolerant algorithms, Distrib. Comput, vol.2, pp.80-94, 1987. ,
Artifact and instructions to generate experimental results for TACAS 2019 paper: Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking (artifact), 2019. ,