@Article{bar-noy:shifting-gears,
  author =       {Amotz Bar-Noy and Danny Dolev and Cynthia Dwork and H. Raymond Strong},
  title =        {Shifting Gears: Changing Algorithms on the Fly to Expedite Byzantine Agreement},
  journal =      {Inf. Comput.},
  year =         1992,
  volume =    97,
  number =    2,
  pages =     {205-233},
}

@InProceedings{ben-or:advantage,
  author =       {Michael Ben-Or},
  title =        {Another advantage of free choice: completely asynchronous agreement protocols},
  booktitle = {Proc. 2nd Symp. Principles of Distributed Computing (PODC 1983)},
  pages =     {27-30},
  year =      1983,
  editor =    {Robert L. Probert and Nancy A. Lynch and Nicola Santoro},
  address =   {Montreal, Canada},
  publisher = {ACM},
}

@inproceedings{biely:tolerating,
 author = {Biely, Martin and Widder, Josef and Charron-Bost, Bernadette and Gaillard, Antoine and Hutle, Martin and Schiper, Andr\'{e}},
 title = {Tolerating corrupted communication},
 booktitle = {Proc. 26th Annual ACM Symposium on Principles of Distributed Computing},
 series = {PODC '07},
 year = {2007},
 isbn = {978-1-59593-616-5},
 location = {Portland, Oregon, USA},
 pages = {244-253},
 numpages = {10},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {byzantine fault tolerance, consensus, dynamic faults, transient faults},
} 

@InProceedings{charron:formal-malicious,
  author =       {Bernadette Charron-Bost and Henri Debrat and Stephan Merz},
  title =        {Formal Verification of Consensus Algorithms Tolerating Malicious Faults},
  booktitle = {13th Intl. Symp. Stabilization, Safety, and Security of Distributed Systems (SSS 2011)},
  pages =     {120-134},
  year =      2011,
  editor =    {Xavier D{\'e}fago and Franck Petit and Vincent Villain},
  volume =    6976,
  series =    {LNCS},
  address =   {Grenoble, France},
  publisher = {Springer},
}

@Article{charron:formal,
  author =       {Bernadette Charron-Bost and Stephan Merz},
  title =        {Formal Verification of a {C}onsensus Algorithm in the {H}eard-{O}f Model},
  journal =      {Intl. J. Software and Informatics},
  volume =       3,
  number =       {2-3},
  pages =        {273--304},
  year =         2009,
}

@Article{charron:heardof,
  author =       {Bernadette Charron-Bost and Andr{\'e} Schiper},
  title =        {The {Heard-Of} model: computing in distributed systems with benign faults},
  journal =      {Distributed Computing},
  year =         2009,
  volume =    22,
  number =    1,
  pages =     {49-71},
}

@article{dwork:consensus,
  Author = "Dwork, C. and N. A. Lynch and L. Stockmeyer",
  Title = "Consensus in the Presence of Partial Synchrony",
  journal = jacm,
  volume = 35,
  number = 2,
  month = apr,
  year = 1988,
  pages = "288--323",
}

@article{FLP85,
  Author = "Fischer, M. J. and N. A. Lynch and M. S. Paterson",
  Title = "Impossibility of Distributed Consensus with one Faulty Process",
  Journal = jacm,
  volume = 32,
  number = 2,
  month = apr,
  Year = 1985,
  pages = "374--382",
}

@Article{jaskelioff:diskpaxos,
  author =       {Mauro Jaskelioff and Stephan Merz},
  title =        {Proving the Correctness of {DiskPaxos}},
  journal =      {Archive of Formal Proofs},
  year =         {2005},
  url = {http://isa-afp.org/entries/DiskPaxos.shtml},
}

@Article{lamport:part-time,
  author =   {Leslie Lamport},
  title =   {The Part-Time Parliament},
  journal =   {ACM Trans. Comput. Syst.},
  year =   1998,
  volume =  16,
  number =  2,
  pages =  {133-169},
}

@Book{lynch:distributed,
  author =   {Nancy Lynch},
  title =   {Distributed Algorithms},
  publisher =   {Morgan Kaufmann Publishers},
  year =   1996,
  address =  {San Mateo, CA}
}

@InProceedings{saad:reduction,
  author =   {Mouna Chaouch-Saad and Bernadette Charron-Bost and Stephan Merz},
  title =   {A Reduction Theorem for the Verification of Round-Based Distributed Algorithms},
  booktitle = {Reachability Problems},
  pages =   {93--106},
  year =   2009,
  editor =   {Olivier Bournez and Igor Potapov},
  volume =   5797,
  series =   {Lecture Notes in Computer Science},
  address =   {Palaiseau, France},
  publisher = {Springer},
}