Conference proceeding
Finding conflicting instances of quantified formulas in SMT
2014 Formal Methods in Computer-Aided Design (FMCAD), pp.195-202
10/2014
DOI: 10.1109/FMCAD.2014.6987613
Abstract
In the past decade, Satisfiability Modulo Theories (SMT) solvers have been used successfully in a variety of applications including verification, automated theorem proving, and synthesis. While such solvers are highly adept at handling ground constraints in several decidable background theories, they primarily rely on heuristic quantifier instantiation methods such as E-matching to process quantified formulas. The success of these methods is often hindered by an overproduction of instantiations which makes ground level reasoning difficult. We introduce a new technique that alleviates this shortcoming by first discovering instantiations that are in conflict with the current state of the solver. The solver only resorts to traditional heuristic methods when such instantiations cannot be found, thus decreasing its dependence upon E-matching. Our experimental results show that our technique significantly reduces the number of instantiations required by an SMT solver to answer "unsatisfiable" for several benchmark libraries, and consequently leads to improvements over state-of-the-art implementations.
Details
- Title: Subtitle
- Finding conflicting instances of quantified formulas in SMT
- Creators
- Andrew Reynolds - University of IowaCesare Tinelli - University of IowaLeonardo de Moura - Microsoft Research (United Kingdom)
- Resource Type
- Conference proceeding
- Publication Details
- 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.195-202
- DOI
- 10.1109/FMCAD.2014.6987613
- Publisher
- FMCAD and the authors
- Language
- English
- Date published
- 10/2014
- Academic Unit
- Computer Science
- Record Identifier
- 9984259500102771
Metrics
14 Record Views