Simplify: a theorem prover for program checking

TLDR

Simplify serves as the proof engine for the Extended Static Checkers ESC/Java and ESC/Modula‑3. The article aims to provide a detailed description of the automatic theorem prover Simplify. Simplify combines decision procedures for several important theories via the Nelson–Oppen method, uses a matcher that reasons about quantifiers by matching up to equivalence in an E‑graph, and incorporates error‑context reporting and error‑localization techniques to help users identify why a false conjecture is false. The article presents detailed performance figures for conjectures derived from realistic program‑checking problems.

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.