towards automatic synthesis of software verification tools
Automatically generated tools can significantly improve programmer productivity. For example, parsers can be automatically generated from declarative specifications in form of grammars, which tremendously simplifies the task of implementing a compiler. In this talk, we present a method for the automatic synthesis of software verification tools. Our synthesis procedure takes as input a description of the employed proof rule, e.g., program safety checking via inductive invariants, and produces a tool that automatically discovers the auxiliary assertions required by the proof rule, e.g., inductive loop invariants and procedure summaries. We rely on a (standard) representation of proof rules using recursive equations over the auxiliary assertions. The discovery of auxiliary assertions, i.e., solving the equations, is based on an iterative process that extrapolates solutions obtained for finitary unrollings of equations. We show how our method synthesizes automatic safety and liveness verifiers for programs with procedures, multi-threaded programs, and higher-order functional programs.
software verification constraint solving automatic tool generation