From Program Verification to Program Synthesis
This paper describes a novel technique for the synthesis of imperative
programs. Automated program synthesis has the potential to make programming
and design of systems easier by allowing the programs to be specified at a
higher-level than executable code. In our approach, which we call
proof-theoretic synthesis, the user provides an input-output functional
specification, a description of the atomic operations in the programming
language, and a specification of the synthesized program's looping structure,
allowed stack space, and bound on usage of certain operations. Our technique
synthesizes a program, if there exists one, that meets the input-output
specification and uses only the given resources.
The insight behind our approach is to interpret program synthesis as
generalized program verification, which allows us to bring verification tools
and techniques to program synthesis. Our synthesis algorithm works by creating
a program with unknown statements, guards, inductive invariants, and ranking
functions. It then generates constraints that relate the unknowns and enforces
three kinds of requirements: partial correctness, loop termination, and
well-formedness conditions on program guards. We formalize the requirements
that program verification tools must meet to solve these constraint and use
off-the-shelf verification tools, from prior work, as our synthesizers.
We demonstrate the feasibility of the proposed approach by synthesizing
programs in three different domains: arithmetic, sorting, and dynamic
programming. Using verification tools, that we built in prior work, for each of
these domains, we are able to synthesize programs for complicated arithmetic
algorithms including Strassen's matrix multiplication and Bresenham's line
drawing; several sorting algorithms; and several dynamic programming algorithms.
For these programs, the median time for synthesis is 14 seconds, and the ratio
of synthesis to verification time ranges between 1X to 92X (with
an median of 7X), illustrating the potential of the approach.