Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties

Derek Egolf, Stavros Tripakis

We present a novel approach for the synthesis of recursive programs from mixed-quantifier first-order logic properties. We solve this problem using a sketching-based, enumerative,…