## Simplify: A Theorem Prover for Program Checking

1 Theorem prover. Uses Nelson-Oppen approach. A part of Extended Static Checking project (ESC). 2 Input: first-order formula, including quantifiers. Theories: equality, linear rational arithmetic, linear integer arithmetic. To check the validity of a conjecture *G*, Simplify tests the satisfiability of ¬*G*. Uses backtracking search.

3 Theory of equality: =. Theory of arithmetic: +, —, ×, >, <, ≥, ≤.

Sergey Vartanov, 2007–2020