Paper Info
Title
Recursion Synthesis with Unrealizability Witnesses
Abstract
We propose SE(2)GIS, a novel inductive recursion synthesis approach with the ability to both synthesize code and declare a problem unsolvable. SE(2)GIS combines a symbolic variant of counterexample-guided inductive synthesis (CEGIS) with a new dual inductive procedure, which focuses on proving a synthesis problem unsolvable rather than finding a solution for it. A vital component of this procedure is a new algorithm that produces a witness, a set of concrete assignments to relevant variables, as a proof that the synthesis instance is not solvable. Witnesses in the dual inductive procedure play the same role that solutions do in classic CEGIS; that is, they ensure progress. Given a reference function, invariants on the input recursive data types, and a target family of recursive functions, SE(2)GIS synthesizes an implementation in this family that is equivalent to the reference implementation, or declares the problem unsolvable and produces a witness for it. We demonstrate that SE(2)GIS is effective in both cases; that is, for interesting data types with complex invariants, it can synthesize non-trivial recursive functions or output witnesses that contain useful feedback for the user.
Year
DOI
Venue
2022
10.1145/3519939.3523726
PROCEEDINGS OF THE 43RD ACM SIGPLAN INTERNATIONAL CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '22)
Keywords
DocType
Citations 
Program Synthesis, Functional Programming, Invariants, Unrealizability, Recursion, Abstraction
Conference
0
PageRank 
References 
Authors
0.34
0
3
Name
Order
Citations
PageRank
Azadeh Farzan100.34
Danya Lette200.34
Victor Nicolet341.54