A New Approach to Recursive Function Synthesis
03/03/2022, 10:30am
Speaker
Abstract
In this talk, I will introduce SE2GIS, a novel inductive recursion synthesis approach with the ability to both synthesize code or declare a problem unsolvable. SE2GIS relies on two innovations for its success: (1) It employs a new partial bounding technique, that selectively bounds a subset of the recursively typed parameters, each by a provably minimal bound. (2) It combines a symbolic variant of counterexample-guided inductive synthesis (CEGIS) with partial bounding with a new dual inductive procedure with a focus on proving synthesis instances unsolvable. The dual inductive routine relies on a new procedure for producing a witness,a set of concrete assignments to relevant variables, as a proof that the synthesis instance is not realizable.
Given a reference function, invariants on the input recursive data types, and a target family of recursive functions, SE2GIS synthesizes an implementation in this family that is equivalent to the reference implementation, or declares the problem unsolvable and produces a witness for it. It can handle interesting recursive data types with complex invariants and synthesize non-trivial recursive functions or output witnesses that contain useful feedback for the user.
This is joint work with my students Victor Nicolet and Danya Lette which is published in two recent papers at CAV'21 and PLDI'22.