Proving the Correctness of Disk Paxos

Title:	Proving the Correctness of Disk Paxos
Author:	Mauro Jaskelioff and Stephan Merz
Submission date:	2005-06-22
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.
Status: [ok]	This is the development version of this entry generated for Isabelle-25-Dec-2009. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any.

Older releases: