| Abstract | 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. \par 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. \par 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. \par 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. |
