TitleUsing simulated execution in verifying distributed algorithms
Publication TypeJournal Article
Year of Publication2004
AuthorsWin T N, Ernst MD, Garland SJ, Kırlı D, Lynch N
JournalSoftware Tools for Technology Transfer
Volume6
Pagination67–76
Date or Month PublishedJuly
AbstractThis paper presents a methodology for using simulated execution to assist a theorem prover in verifying safety properties of distributed systems. Execution-based techniques such as testing can increase confidence in an implementation, provide intuition about behavior, and detect simple errors quickly. They cannot by themselves demonstrate correctness. However, they can aid theorem provers by suggesting necessary lemmas and providing tactics to structure proofs. This paper describes the use of these techniques in a machine-checked proof of correctness of the Paxos algorithm for distributed consensus.
Downloadshttps://homes.cs.washington.edu/~mernst/pubs/simexecution-vmcai2003-slid... slides (PDF) https://homes.cs.washington.edu/~mernst/pubs/simexecution-vmcai2003-slid... slides (PowerPoint) https://homes.cs.washington.edu/~mernst/pubs/simexecution-sttt2004.pdf PDF
Citation KeyNeWinEGKL04:STTT