Simplify: a theorem prover for program checking
Top Cited Papers
- 1 May 2005
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 52 (3), 365-473
- https://doi.org/10.1145/1066100.1066102
Abstract
This article 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 article describes two techniques, error context reporting and error localization, for helping the user to determine the reason that a false conjecture is false. The article includes detailed performance figures on conjectures derived from realistic program-checking problems.Keywords
This publication has 23 references indexed in Scilit:
- The Cassowary linear arithmetic constraint solving algorithmACM Transactions on Computer-Human Interaction, 2001
- GRASP: a search algorithm for propositional satisfiabilityInternational Conference on Acoustics, Speech, and Signal Processing (ICASSP), 1999
- Validity checking for combinations of theories with equalityPublished by Springer Science and Business Media LLC ,1996
- Variations on the Common Subexpression ProblemJournal of the ACM, 1980
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980
- Simplification by Cooperating Decision ProceduresACM Transactions on Programming Languages and Systems, 1979
- A Practical Decision Procedure for Arithmetic with Function SymbolsJournal of the ACM, 1979
- Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysisArtificial Intelligence, 1977
- Efficiency of a Good But Not Linear Set Union AlgorithmJournal of the ACM, 1975
- An improved equivalence algorithmCommunications of the ACM, 1964