On Integrating Deductive Synthesis and Verification Systems
This work addresses the challenge of creating verified programs from relational specifications, which is important for developers in formal methods and software verification, though it appears incremental as it builds on existing frameworks.
The paper tackled the problem of synthesizing and verifying recursive functional programs over unbounded domains by developing new counterexample-guided algorithms, resulting in a system that successfully synthesized useful recursive functions for manipulating unbounded numbers and data structures.
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.