Synthesizing software verifiers from proof rules

TLDR

Automatically generated tools, such as parsers and dataflow analyzers derived from declarative specifications, can greatly improve programmer productivity by simplifying compiler implementation. The paper proposes a method for automatically synthesizing software verification tools. The method takes a proof rule description, represents it with recursive equations over auxiliary assertions, and iteratively solves these equations by extrapolating solutions from finitary unrollings to automatically discover the needed assertions such as loop invariants and procedure summaries. The approach successfully synthesizes safety and liveness verifiers for procedural, multi‑threaded, and functional programs, and experimental comparisons demonstrate its practicality relative to state‑of‑the‑art tools.

Abstract

Automatically generated tools can significantly improve programmer 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 implementing a compiler. In this paper, 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 functional programs. Our experimental comparison of the resulting verifiers with existing state-of-the-art verification tools confirms the practicality of the approach.