: A Theorem Prover for Program Checking
1 Theorem prover. Uses 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