Logo image
Back
Finite Model Finding in SMT
Book chapter   Open access   Peer reviewed

Finite Model Finding in SMT

Andrew Reynolds, Cesare Tinelli, Amit Goel and Sava Krstić
Computer Aided Verification, pp.640-655
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2013
DOI: 10.1007/978-3-642-39799-8_42
url
https://doi.org/10.1007/978-3-642-39799-8_42View
Published (Version of record) Open Access

Abstract

SMT solvers have been used successfully as reasoning engines for automated verification. Current techniques for dealing with quantified formulas in SMT are generally incomplete, forcing SMT solvers to report “unknown” when they fail to prove the unsatisfiability of a formula with quantifiers. This inability to return counter-models limits their usefulness in applications that produce quantified verification conditions. We present a novel finite model finding method that reduces these limitations in the case of quantifiers ranging over free sorts. Our method contrasts with previous approaches for finite model finding in first-order logic by not relying on the introduction of domain constants for the free sorts and by being fully integrated into the general architecture used by most SMT solvers. This integration is achieved through the addition of a novel solver for sort cardinality constraints and a module for quantifier instantiation over finite domains. Initial experiments with verification conditions generated from a deductive verification tool developed at Intel Corp. show that our approach compares quite favorably with the state of the art in SMT.
 Cardinality Constraint Current Assignment Domain Constant Ground Clause Theory Solver

Details

Metrics

26 Record Views
Logo image