Armin Biere, Robert Brummayer,
"Lemmas on Demand for the Extensional Theory of Arrays"
, in Journal on Satisfiability, Boolean Modeling and Computation, Vol. 6, Seite(n) 165-201, 2009, ISSN: 1875-5011
Original Titel:
Lemmas on Demand for the Extensional Theory of Arrays
Sprache des Titels:
Englisch
Original Kurzfassung:
The quantifier-free extensional theory of arrays TA plays an important role in hardware
and software verification. In this article we present a novel decision procedure that
refines formula abstractions with lemmas on demand. We consider the case where TA is
combined with a decidable quantifier-free first-order theory TB. Unlike traditional lazy
SMT approaches, where lemmas are added on the boolean abstraction layer, our decision
procedure adds lemmas in TB. We discuss our decision procedure in detail. In particular,
we prove soundness and completeness, and discuss complexity. We present our decision
procedure in a generic context and provide implementation details and optimizations, in
particular for bit-vectors. Finally, we report on experiments and discuss related work.
Sprache der Kurzfassung:
Englisch
Journal:
Journal on Satisfiability, Boolean Modeling and Computation
Forschungs-