CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
Home Page FCT/UNL UNL
  Home  \  Seminars @ CITI  \  Seminar Page Login  
   
banner bottom
File Top
Synthesizing Software Verifiers from Proof Rules
{ Wed, 17 Oct 2012, 14h00 }

By: Nuno Lopes  [ show info ]

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.


Hosted by: Software Systems

Location: DI seminars room

File Bottom