Model Finding for Recursive Functions in SMT

Abstract : SMT solvers have recently been extended with techniques for finding models in presence of universally quantified formulas in some restricted fragments. This paper introduces a translation which reduces axioms specifying a large class of recursive functions, including well-founded (terminating) functions, to universally quantified formulas for which these techniques are applicable. An empirical evaluation confirms that the approach improves the performance of existing solvers on benchmarks from two sources. The translation is implemented as a preprocessor in the solver CVC4.
Type de document :
Communication dans un congrès
SMT Workshop 2015, Jul 2015, San Francisco, United States. 2015, 〈http://smt2015.csl.sri.com〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01242509
Contributeur : Jasmin Christian Blanchette <>
Soumis le : samedi 12 décembre 2015 - 20:23:59
Dernière modification le : lundi 20 novembre 2017 - 15:14:02
Document(s) archivé(s) le : samedi 29 avril 2017 - 12:16:58

Fichier

shortv.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01242509, version 1

Collections

Citation

Andrew Reynolds, Jasmin Christian Blanchette, Cesare Tinelli. Model Finding for Recursive Functions in SMT. SMT Workshop 2015, Jul 2015, San Francisco, United States. 2015, 〈http://smt2015.csl.sri.com〉. 〈hal-01242509〉

Partager

Métriques

Consultations de la notice

96

Téléchargements de fichiers

48