Viktor Kuncak, Etienne Kneuss, Philippe Paul Henri Suter, Ivan Kuraj
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 synt ...
2013
