Connecting specifications, executions, and proofs: Reducing human interaction in theorem proving

TitleConnecting specifications, executions, and proofs: Reducing human interaction in theorem proving
Publication TypeMiscellaneous
Year of Publication2002
AuthorsWin T N, Ernst MD, Garland SJ
Abstract<p>Using a theorem prover to verify that distributed systems meet their formal specifications can require substantial human interaction. A promising technique for reducing the amount of interaction required uses dynamic (run-time) program analysis to automatically discover likely program invariants, which are suitable for use as lemmas in the verification process. This paper describes a collection of tools that provide support for this technique, as well as their application to several well known distributed algorithms.</p>
Citation KeyNeWinEG:connecting
Last changed Mon, 2013-06-03 10:27