Proving the Correctness of Disk Paxos

Mauro Jaskelioff 🌐 and Stephan Merz 🌐

June 22, 2005

Abstract

Disk Paxos is an algorithm for building arbitrary fault-tolerant distributed systems. The specification of Disk Paxos has been proved correct informally and tested using the TLC model checker, but up to now, it has never been fully formally verified. In this work we have formally verified its correctness using the Isabelle theorem prover and the HOL logic system, showing that Isabelle is a practical tool for verifying properties of TLA+ specifications.

License

BSD License

Topics

Session DiskPaxos

Cite

× 
@article{DiskPaxos-AFP,
  author  = {Mauro Jaskelioff and Stephan Merz},
  title   = {Proving the Correctness of Disk Paxos},
  journal = {Archive of Formal Proofs},
  month   = {June},
  year    = {2005},
  note    = {\url{https://isa-afp.org/entries/DiskPaxos.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: