Verifying and Synthesizing Software with Recursive Functions (Invited Contribution)

Abstract. Our goal is to help people construct software that does what they wish. We develop tools and algorithms that span static and dynamic verification, constraint solving, and program synthesis. I will outline the current state our verification and synthesis system, Leon, which trans-lates software into a functional language and uses SMT solvers to reason about paths in programs and specifications. Certain completeness results partly explain the effectiveness of verification and synthesis procedures implemented within Leon, in particular results on decidability of suffi-ciently surjective abstraction functions, and the framework of complete functional synthesis.