Model Finding for Recursive Functions in SMT - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2015

Model Finding for Recursive Functions in SMT

Résumé

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.
Fichier principal
Vignette du fichier
shortv.pdf (173.26 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01242509 , version 1 (12-12-2015)

Identifiants

  • HAL Id : hal-01242509 , version 1

Citer

Andrew Reynolds, Jasmin Christian Blanchette, Cesare Tinelli. Model Finding for Recursive Functions in SMT. SMT Workshop 2015 - 13th International Workshop on on Satisfiability Modulo Theories, Jul 2015, San Francisco, United States. ⟨hal-01242509⟩
223 Consultations
94 Téléchargements

Partager

Gmail Facebook X LinkedIn More