Paper Info
Title
Towards automatic synthesis of software verification tools
Abstract
Automatically generated tools can significantly improve programmer productivity. For example, parsers can be automatically generated from declarative specifications in form of grammars, which tremendously simplifies the task of implementing a compiler. In this talk, 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 higher-order functional programs.
Year
DOI
Venue
2011
10.1007/978-3-642-31759-0_3
SPIN'12 Proceedings of the 19th international conference on Model Checking Software
Keywords
DocType
Citations 
application domain,program safety checking,declarative specification,towards automatic synthesis,synthesis procedure,inductive invariants,security critical system,automatic safety,automatic synthesis,tedious aspect,auxiliary assertion,proof rule,software verification tool,software verification,software reliability,large number,creative aspect,inductive loop invariants,software complexity,software verifier development,procedure summary,higher order functions
Conference
0
PageRank 
References 
Authors
0.34
1
1
Name
Order
Citations
PageRank
Andrey Rybalchenko1143968.53