Template-based program verification and program synthesis |
| |
Authors: | Saurabh Srivastava Sumit Gulwani Jeffrey S Foster |
| |
Affiliation: | 1. University of California, Berkeley, CA, USA 2. Microsoft Research, Redmond, WA, USA 3. University of Maryland, College Park, MD, USA
|
| |
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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|