A. Bar-noy, D. Dolev, C. Dwork, and H. R. Strong, Shifting gears: Changing algorithms on the fly to expedite Byzantine agreement, Information and Computation, pp.42-51, 1987.

M. Biely, J. Widder, B. Charron-bost, A. Gaillard, M. Hutle et al., Tolerating corrupted communication, Proceedings of the twenty-sixth annual ACM symposium on Principles of distributed computing, PODC '07, pp.244-253, 2007.
DOI : 10.1145/1281100.1281136
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.173.6474

M. Chaouch-saad, B. Charron-bost, and S. Merz, A Reduction Theorem for the Verification of Round-Based Distributed Algorithms, 3rd Workshop on Reachability Problems, pp.93-106, 2009.
DOI : 10.1007/3-540-48153-2_6
URL : https://hal.archives-ouvertes.fr/inria-00408908

B. Charron-bost and S. Merz, Formal verification of a Consensus algorithm in the Heard-Of model, Int. J. Software and Informatics, vol.3, issue.2-3, pp.273-303, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00426388

B. Charron-bost and A. Schiper, The Heard-Of model: Computing in distributed systems with benign failures, Distributed Computing, 2009.

C. Dwork, N. A. Lynch, and L. Stockmeyer, Consensus in the presence of partial synchrony, Journal of the ACM, vol.35, issue.2, pp.288-323, 1988.
DOI : 10.1145/42282.42283

T. Elrad and N. Francez, Decomposition of distributed programs into communication-closed layers, Science of Computer Programming, vol.2, issue.3, 1982.
DOI : 10.1016/0167-6423(83)90013-8

M. J. Fischer, N. A. Lynch, and M. S. Paterson, Impossibility of distributed consensus with one faulty process, Journal of the ACM, vol.32, issue.2, pp.374-382, 1985.
DOI : 10.1145/3149.214121

C. Georgiou, N. A. Lynch, P. Mavrommatis, and J. A. Tauber, Automated implementation of complex distributed algorithms specified in the IOA language, International Journal on Software Tools for Technology Transfer, vol.21, issue.9, pp.153-171, 2009.
DOI : 10.1007/s10009-008-0097-7

W. H. Hesselink, The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract, Formal Aspects of Computing, vol.11, issue.1, pp.45-55, 1999.
DOI : 10.1007/s001650050035

M. Jaskelioff and S. Merz, Proving the correctness of Disk Paxos Archive of Formal Proofs, 2005.

L. Lamport, What good is temporal logic?, Information Processing 83: Proceedings of the IFIP 9th World Congress, pp.657-668, 1983.

L. Lamport, Byzantining Paxos by refinement, 2010.
DOI : 10.1007/978-3-642-24100-0_22

L. Lamport and S. Merz, Specifying and verifying fault-tolerant systems, 3rd Intl. Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'94), pp.41-76, 1994.
DOI : 10.1007/3-540-58468-4_159

N. A. Lynch, Distributed Algorithms, 1996.

T. Nipkow, L. Paulson, M. Wenzel, /. Isabelle, and . Hol, A Proof Assistant for Higher-Order Logic, LNCS, vol.2283, 2002.

D. Peled and T. Wilke, Stutter-invariant temporal properties are expressible without the next-time operator, Proc. Letters, pp.243-246, 1997.
DOI : 10.1016/S0020-0190(97)00133-6

U. Schmid, B. Weiss, and J. M. Rushby, Formally verified Byzantine agreement in presence of link faults, Proceedings 22nd International Conference on Distributed Computing Systems, pp.608-616, 2002.
DOI : 10.1109/ICDCS.2002.1022311

T. Tsuchiya and A. Schiper, Model checking of consensus algorithms, 26th IEEE Symp. Reliable Distributed Systems (SRDS 2007), pp.137-148, 2007.

T. Tsuchiya and A. Schiper, Using Bounded Model Checking to Verify Consensus Algorithms, 22nd Intl. Symp. Dist. Comp. (DISC 2008), pp.466-480, 2008.
DOI : 10.1007/978-3-540-87779-0_32