Kneuss, EtienneKuncak, ViktorKuraj, IvanSuter, Philippe2013-04-182013-04-182013-04-182013https://infoscience.epfl.ch/handle/20.500.14299/91592We 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.program synthesisverificationsoftware reliabilityfunctional programmingcounterexample-guided synthesisdeductive synthesisLeontext::report