H. Attiya and J. Welch, , 2004.

M. Barnett, B. E. Chang, R. Deline, B. Jacobs, and K. R. Leino, Boogie: A modular reusable verifier for object-oriented programs, Formal Methods for Components and Objects, pp.364-387, 2005.

F. V. Brasileiro, F. Greve, A. Mostéfaoui, and M. Raynal, Consensus in one communication step. In: PaCT. LNCS, vol.2127, pp.42-50, 2001.

L. De-moura and N. Bjørner, Z3: An efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, vol.1579, pp.337-340, 2008.

D. Dobre and N. Suri, One-step consensus with zero-degradation, DSN. pp, pp.137-146, 2006.

R. Guerraoui, Non-blocking atomic commit in asynchronous distributed systems with failure detectors, Distributed Computing, vol.15, issue.1, pp.17-25, 2002.

G. Holzmann, The SPIN Model Checker, 2003.
DOI : 10.1109/32.588521

A. John, I. Konnov, U. Schmid, H. Veith, and J. Widder, Parameterized model checking of fault-tolerant distributed algorithms by abstraction, FMCAD. pp, pp.201-209, 2013.
DOI : 10.1109/fmcad.2013.6679411

A. John, I. Konnov, U. Schmid, H. Veith, and J. Widder, Towards modeling and model checking fault-tolerant distributed algorithms, SPIN. LNCS, vol.7976, pp.209-226, 2013.
DOI : 10.1007/978-3-642-39176-7_14
URL : http://spinroot.com/spin/Workshops/ws13/spin2013_submission_28.pdf

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.

I. Konnov, H. Veith, and J. Widder, On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability, CONCUR. LNCS, vol.8704, pp.125-140, 2014.

I. Konnov, H. Veith, and J. Widder, SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms, CAV (Part I), vol.9206, pp.85-102, 2015.
DOI : 10.1007/978-3-319-21690-4_6

I. Konnov, H. Veith, and J. Widder, What you always wanted to know about model checking of fault-tolerant distributed algorithms, PSI 2015, in Memory of Helmut Veith, Revised Selected Papers, vol.9609, pp.6-21, 2016.

I. V. Konnov, J. Widder, F. Spegni, and L. Spalazzi, Accuracy of message counting abstraction in fault-tolerant distributed algorithms, VMCAI. pp, pp.347-366, 2017.

M. Lazic, I. Konnov, J. Widder, and R. Bloem, Synthesis of distributed algorithms with parameterized threshold guards, OPODIS. LIPIcs, vol.95, p.20, 2017.

N. Lynch, Distributed Algorithms, 1996.

O. Mari´cmari´c, C. Sprenger, and D. A. Basin, Cutoff Bounds for Consensus Algorithms, CAV. pp, pp.217-237, 2017.

A. Mostéfaoui, E. Mourgaya, P. R. Parvédy, and M. Raynal, Evaluating the conditionbased approach to solve consensus, pp.541-550, 2003.

M. Pease, R. Shostak, and L. Lamport, Reaching agreement in the presence of faults, J.ACM, vol.27, issue.2, pp.228-234, 1980.

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

Y. J. Song and R. Van-renesse, Bosco: One-step Byzantine asynchronous consensus, DISC. LNCS, vol.5218, pp.438-450, 2008.
DOI : 10.1007/978-3-540-87779-0_30
URL : http://www.cs.cornell.edu/projects/quicksilver/public_pdfs/52180438.pdf

T. Srikanth and S. Toueg, Simulating authenticated broadcasts to derive simple faulttolerant algorithms, Dist. Comp, vol.2, pp.80-94, 1987.

O. Tange, Gnu parallel-the command-line power tool. The USENIX Magazine, vol.36, pp.42-47, 2011.

L. Tseng, Voting in the presence of byzantine faults, Dependable Computing (PRDC), pp.1-10, 2017.