Verifying and Synthesizing Software with Recursive Functions (Invited Contribution)

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.


Editor(s):
Esparza, J
Fraigniaud, P
Husfeldt, T
Koutsoupias, E
Published in:
Automata, Languages, And Programming (Icalp 2014), Pt I, 8572, 11-25
Presented at:
41st International Colloquium on Automata, Languages and Programming
Year:
2014
Publisher:
Berlin, Springer-Verlag Berlin
ISSN:
0302-9743
ISBN:
978-3-662-43948-7
Laboratories:




 Record created 2015-05-29, last modified 2018-09-13


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)