Connecting specifications, executions, and proofs: Reducing human interaction in theorem proving
Submitted by mernst on Wed, 2011-11-30 14:35
| Title | Connecting specifications, executions, and proofs: Reducing human interaction in theorem proving |
| Publication Type | Miscellaneous |
| Year of Publication | 2002 |
| Authors | Win 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 Key | NeWinEG:connecting |
Last changed Mon, 2013-06-03 10:27

cs.