For the verification part, the main paper is "Satisfiability Modulo Recursive Programs", SAS 2011 [1]. For the synthesis part, the most up-to-date paper is "Syn

For the verification part, the main paper is "Satisfiability Modulo Recursive Programs", SAS 2011 [1]. For the synthesis part, the most up-to-date paper is "Synthesis Modulo Recursive Functions", OOPSLA 2013 [2]. As is usual with CS papers, searching for the title in your favorite search engine may or may not help you find a PDF version. I'm an author on both papers, so feel free to ask any questions here as well. [1] http://link.springer.com/chapter/10.1007%2F978-3-642-23702-7_23 http://link.springer.com/chapter/10.1007%2F978-3-642-23702-7... [2] http://dl.acm.org/citation.cfm?id=2509555 http://dl.acm.org/citation.cfm?id=2509555