Synthesizing Software Verifiers from Proof Rules

Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko

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.

Published:

S. Grebenshchikov, N. P. Lopes, C. Popeea, A. Rybalchenko. Synthesizing Software Verifiers from Proof Rules. In Proc. of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2012 (HVC'14 Award).

Download:

Bibtex:

@inproceedings{hsf-pldi12,
  title =	{Synthesizing Software Verifiers from Proof Rules},
  author =	{Sergey Grebenshchikov and Nuno P. Lopes and Corneliu Popeea and Andrey Rybalchenko},
  booktitle =	{Proc. of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)},
  doi =		{10.1145/2254064.2254112},
  month =	jun,
  year =	2012
}

Copyright notice:

<-- Return