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 translates 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 sufficiently surjective abstraction functions, and the framework of complete functional synthesis. © 2014 Springer-Verlag.
Cite
CITATION STYLE
Kuncak, V. (2014). Verifying and synthesizing software with recursive functions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8572 LNCS, pp. 11–25). Springer Verlag. https://doi.org/10.1007/978-3-662-43948-7_2
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
