DiskPaxos (Q40950)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry DiskPaxos
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | DiskPaxos |
AFP entry DiskPaxos |
Statements
Mauro Jaskelioff
0 references
Stephan Merz
0 references
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.
0 references
22 June 2005
0 references
Proving the Correctness of Disk Paxos (English)
0 references
