On Integrating Deductive Synthesis and Verification Systems

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 synthesis procedures for algebraic data types. We present new counterexample-guided algorithms for constructing verified programs. We have implemented these algorithms in an integrated environment for interactive verification and synthesis from relational specifications. Our system was able to synthesize a number of useful recursive functions that manipulate unbounded numbers and data structures.


Année
2013
Publisher:
EPFL
Mots-clefs:
Laboratoires:




 Notice créée le 2013-04-18, modifiée le 2019-12-05

n/a:
Télécharger le documentPDF
Lien externe:
Télécharger le documentURL
Évaluer ce document:

Rate this document:
1
2
3
 
(Pas encore évalué)