Kneuss, Etienne
Kuncak, Viktor
Kuraj, Ivan
Suter, Philippe
Synthesis Modulo Recursive Functions
Acm Sigplan Notices
0362-1340
10.1145/2509136.2509555
48
10
407-426
20
We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo recursive functions, a framework for deductive synthesis, and complete synthesis procedures for algebraic data types. We present new counterexample-guided algorithms for constructing verified programs. We have implemented these algorithms in an integrated environment for interactive verification and synthesis from relational specifications. Our system was able to synthesize a number of useful recursive functions that manipulate unbounded numbers and data structures.
software synthesis;
inductive learning;
satisfiability modulo theories;
2013