Download: PDF, PostScript.
“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.
We use output from dynamic analysis to assist theorem-proving of safety properties of distributed algorithms. The algorithms are written in the IOA language, which is based on the mathematical I/O automaton model. Daikon, a dynamic invariant discovery tool, generalizes from test executions, producing assertions about the observed behavior of the algorithm.
We use these relatively simple run-time properties as lemmas in proving program properties. These lemmas are necessary, but easy for humans to overlook. Furthermore, the lemmas decompose complex steps into simple ones that theorem provers can manage mostly unassisted, thus reducing the human effort required to prove interesting algorithm properties.
In several experiments, Daikon produced all or most of the lemmas required for correctness proofs, automating the most difficult part of the process, which usually requires human insight.
This verification technique is a worthwhile alternative to using only static analysis with model checkers or theorem provers, or only dynamic analysis with simulators and runtime analyzers. Our technique combines the advantages of static and dynamic analysis: it is sound and scales to algorithms with unbounded processes and variable sizes. Further, it can suggest and verify new program properties that the designer might not have envisioned.
Download: PDF, PostScript.
BibTeX entry:
@techreport{NeWinE02:TR841,
author = {Ne Win, Toh and Michael D. Ernst},
title = {Verifying distributed algorithms via dynamic analysis and
theorem proving},
institution = {MIT Laboratory for Computer Science},
number = {841},
address = {Cambridge, MA},
month = {May~25,},
year = {2002}
}
(This webpage was created with bibtex2web.)
Back to Program Analysis Group publications.