Synthesizing software verifiers from proof rules

Automatically generated tools can significantly improve program-mer productivity. For example, parsers and dataflow analyzers can be automatically generated from declarative specifications in the form of grammars, which tremendously simplifies the task of im-plementing a compiler. In this paper, we present a method for the automatic synthesis of software verification tools. Our synthe-sis 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 asser-tions 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 asser-tions. The discovery of auxiliary assertions, i.e., solving the equa-tions, 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 pro-grams with procedures, multi-threaded programs, and functional programs. Our experimental comparison of the resulting verifiers with existing state-of-the-art verification tools confirms the practi-cality of the approach