Sciweavers

POPL
2010
ACM

From Program Verification to Program Synthesis

14 years 21 days ago
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 the design of systems easier by allowing 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 inputoutput 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 invaria...
Saurabh Srivastava, Sumit Gulwani, Jeffrey S. Fost
Added 01 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where POPL
Authors Saurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster
Comments (0)