Publication
“Using simulated execution in verifying distributed algorithms”
Toh Ne Win, Michael D. Ernst, Stephen J. Garland,
Dilsun Kırlı, and Nancy Lynch
Software Tools for
Technology Transfer 6:1, July 2004, pages 67-76.
A previous version appeared in
VMCAI'03, Fourth International
Conference on Verification, Model Checking and Abstract
Interpretation, (New York, New York), January 9-11, 2003, pages
283-297.
Additional details and case studies appeared as
“Verifying distributed algorithms via dynamic analysis and
theorem proving”
by Toh Ne Win and Michael D. Ernst,
MIT Laboratory for Computer Science Technical Report 841, May 25, 2002.
Abstract
This 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.
Download:
PDF