ADI: Automatic Derivation of Invariants

Most current systems for mechanical program verification are not fully automatic, since the user himself must provide the intermediate inductive assertions. This paper describes an interactive computer program, called ADI, which automatically generates the needed inductive assertions. ADI is also able to extend partial loop assertions supplied by the user to form complete assertions. The implementation (written in QLISP and INTERLISP) is based on both the algorithmic and the heuristic approaches introduced by Katz and Manna in "Logical Analysis of Programs" [25]. For the algorithmic subsystem ADI includes: Difference Equations Constructor, Difference Equations Solver, and Invariants from Conditional Statements Generator. The heuristic subsystem includes: Exit Rules Package, Bounding Variables Component, Strengthening Executer, Weakening Executer, and a Heuristic Invariant Matcher-which is the actual implementation of two new heuristics, MATCHPQ and MATCHPT. ADI is a small step toward interactive, practical program verification.