salle A. Turing CE4
13 septembre 2012 - 14h00
Synthesizing Software Verifiers from Proof Rules
par Corneliu Popeea de Technical University of Munich
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 talk, I will present a method for the automatic synthesis of
software verification tools. The 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.
I will show how our method synthesizes automatic safety and liveness
verifiers for programs with procedures, multi-threaded programs, and
functional programs. The experimental comparison of the resulting
verifiers with existing state-of-the-art verification tools confirms
the practicality of the approach.
This is joint work with Sergey Grebenshchikov, Nuno Lopes and Andrey
Rybalchenko at the Technical University Munich.
