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.