In formal verification, we ultimately rely on automatic provers to decide whether formulas are valid (always true) or not. In GNATprove for example, we rely mostly on the ability of prover Alt-Ergo to analyze quickly the formulas we generate, and answer yes when the formula is valid or no when the formula is invalid (so there is a problem with the code or the assertions in the program). The reality is that the prover may take a long time to reply yes/no, and that in some cases it just replies I don’t know!
A promising approach to help automatic provers answer more quickly is to reduce the size of the formula. Typically, this formula contains thousands of axioms defining all relevant symbols from the program (functions, types, constants), as well as describing the context in which the formula should hold (typically a path or set of paths through a function, as produced by a verification condition generator). Researchers have proposed strategies to start with a small subset of these axioms, and incrementally grow it until a proof is found. At AdaCore, Duc Hoang is ending today a 6 months internship on that subject.
We have devised a strategy based on definition links, as in the work of Josef Urban (”An overview of methods for large-theory automated theorem proving”) and SInE, with a graph-based approach, similar to the work of Couchot et al. (”A graph-based strategy for the selection of hypotheses” & “Graph Based Reduction of Program Verification Conditions”).
This work is publicly available, if others want to try it out (main switch is -autoselect), in the git repository for our version of Alt-Ergo:
git clone https://forge.open-do.org/anonscm/git/alt-ergo/alt-ergo.git
We had a discussion a few days ago on this subject and others related to Alt-Ergo with CEA-LIST research lab and OCamlPro company, both interested in a shared development of Alt-Ergo. If you are also interested in joining this effort, contact us at AdaCore.