Using simulated execution in verifying distributed algorithms

Download: PDF, slides (PDF), slides (PowerPoint).

“Using simulated execution in verifying distributed algorithms” by Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kırlı, and Nancy Lynch. Software Tools for Technology Transfer, vol. 6, no. 1, July 2004, pp. 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, pp. 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, (Cambridge, MA), May 25, 2002.


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, slides (PDF), slides (PowerPoint).

BibTeX entry:

   author = {Ne Win, Toh and Michael D. Ernst and Stephen J. Garland and
	Dilsun K{\i}rl{\i} and Nancy Lynch},
   title = {Using simulated execution in verifying distributed algorithms},
   journal = {Software Tools for Technology Transfer},
   volume = {6},
   number = {1},
   pages = {67--76},
   month = jul,
   year = {2004}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.