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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/hal-01242509
Contributor : Jasmin Christian Blanchette <>
Submitted on : Saturday, December 12, 2015 - 8:23:59 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Document(s) archivé(s) le : Saturday, April 29, 2017 - 12:16:58 PM

File

shortv.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-01242509⟩

Share

Metrics

Record views

233

Files downloads

75