Simplify: a theorem prover for program checking

By David Detlefs, Greg Nelson, J. Saxe. JACM, 2005

959 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/8c45e059a11b1c6398b45c92610804e1f28336d4

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

Citations in the corpus

A Fast Linear-Arithmetic Solver for DPLL(T) (2006, methodology): “The common methods for integrating a Simplex solver with DPLL rely on incremental versions of Simplex such as described in [11,12,13,14].”
Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution (2005, methodology): “In these experiments , we have used the Simplify [14] theorem prover to check unsatisfiability of path conditions, the Omega library [28] to check implications, and the POOC constraint solver [31] to solve constraints.”
Z3: An Efficient SMT Solver (2008, methodology): “Equalities asserted by the SAT solver are propagated by the congruence closure core using a data structure that we will call an E-graph following [8].”
The YICES SMT Solver (2006, methodology): “The main approach is an extension of egraph matching[4] that supports offset equalities and terms.”
isl: An Integer Set Library for the Polyhedral Model (2010, methodology): “The core of the library is formed by an incremental LP solver modeled after that of Simplify [10].”
DreamCoder: bootstrapping inductive program synthesis with wake-sleep library learning (2021, methodology): “The algorithm leverages E-graph matching [11] to identify rewrites to the original programs that may expose more common patterns.”
The software model checker Blast (2007, methodology): “The decision procedures underlying BLAST, which are used for computing reachable regions and interpolants of path formulas, implement linear arithmetic and uninterpreted functions [31, 64, 71].”
egg: Fast and extensible equality saturation (2020, methodology): “Traditionally [Detlefs et al. 2005; Nelson 1980], e-graphs maintain their data structure invariants after each operation.”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, methodology): “This approach is used with the theory solver for the quantiﬁer-free fragment of the theory of equality with uninterpreted functions (EUF) and with the quantiﬁer-instantiation technique based on E-matching with triggers [53,89].”
Semantic code search via equational reasoning (2020, background): “(defsearch bound-checking (root <- (generic/binop :or (generic/binop :< x lo) (generic/binop :>= x hi)))) Of course, our worked example only shows Yogo reasoning about pure code, using the classic techniques of e-graphs and congruence-closure [10, 50, 51].”
The Spec# Programming System: An Overview (2004, methodology): “Currently, Boogie uses the Simplify theorem prover [18], but we intend to switch to a new experimental theorem prover being developed at Microsoft Research.”
A Survey of Automated Techniques for Formal Software Verification (2008, methodology): “In counterexample-guided abstraction refinement [7], [37], [87] (CEGAR), if model checking the abstraction yields a counterexample that does not exist in the concrete program, the abstract counterexample is used to identify new predicates and to obtain a more precise abstraction.”
An overview of JML tools and applications (2003, methodology): “Under the hood, ESC/Java is powered by detailed program semantics and an automatic (noninteractive) theorem prover, Simplify [26].”
Computer-Aided Security Proofs for the Working Cryptographer (2011, methodology): “We then use the Simplify prover [16] and the alt-ergo SMT solver [13] to discharge the conditions (although many others provers are supported, including interactive theorem provers such as Coq).”