Paper Info
Title
Template-based program verification and program synthesis.
Abstract
Program verification is the task of automatically generating proofs for a program’s compliance with a given specification. Program synthesis is the task of automatically generating a program that meets a given specification. Both program verification and program synthesis can be viewed as search problems, for proofs and programs, respectively. For these search problems, we present approaches based on user-provided insights in the form of templates. Templates are hints about the syntactic forms of the invariants and programs, and help guide the search for solutions. We show how to reduce the template-based search problem to satisfiability solving, which permits the use of off-the-shelf solvers to efficiently explore the search space. Template-based approaches have allowed us to verify and synthesize programs outside the abilities of previous verifiers and synthesizers. Our approach can verify and synthesize difficult algorithmic textbook programs (e.g., sorting and dynamic programming-based algorithms) and difficult arithmetic programs.
Year
DOI
Venue
2013
10.1007/s10009-012-0223-4
STTT
Keywords
DocType
Volume
Synthesis, Verification, Template-based program analyses, SMT solvers, Pre-and postcondition inference, Static analysis, Predicate abstraction, Human guided verification and synthesis
Journal
15
Issue
ISSN
Citations 
5-6
1433-2787
27
PageRank 
References 
Authors
0.83
29
3
Name
Order
Citations
PageRank
Saurabh Srivastava118419.27
Sumit Gulwani22263110.91
Jeffrey S. Foster32035174.45