Detail

Synthesizing Software Verifiers from Proof Rules

In this talk, I’ll 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.
I’ll 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.

Paper published in PLDI’12. Joint work with Sergey Grebenshchikov, Corneliu
Popeea, and Andrey Rybalchenko.