| |
Click here for full text:
Simplify: A Theorem Prover for Program Checking
Detlefs, David; Nelson, Greg; Saxe, James B.
HPL-2003-148
Keyword(s): theorem-proving; decision procedures; program checking
Abstract: This paper provides a detailed description of the automatic theorem prover Simplify, which is the proof engine of the Extended Static Checkers ESC/Java and ESC/Modula-3. Simplify uses the Nelson-Oppen method to combine decision procedures for several important theories, and also employs a matcher to reason about quantifiers. Instead of conventional matching in a term DAG, Simplify matches up to equivalence in an E- graph, which detects many relevant pattern instances that would be missed by the conventional approach. The paper describes two techniques, labels and counterexample contexts, for helping the user to determine the reason that a false conjecture is false. The paper includes detailed performance figures on conjectures derived from realistic program-checking problems. Notes:
121 Pages
Back to Index
|
printable version
