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 specication. Program synthesis is the task of automatically generating a program that meets a given specication. Both program verication 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 satisability solving, which permits the use of off-the-shelf solvers to eciently 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 dicult algorithmic textbook programs (e.g., sorting, and dynamic programming-based algorithms, etc.), and difficult arithmetic programs.