Robert Brummayer, Armin Biere,
"Effective Bit-Width and Under-Approximation"
: Proc. 12th Intl. Conference on Computer Aided Systems Theory (EUROCAST'09), Lecture Notes in Computer Science (LNCS), Vol. 5717, Seite(n) 304-311, 2-2009
Original Titel:
Effective Bit-Width and Under-Approximation
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 12th Intl. Conference on Computer Aided Systems Theory (EUROCAST'09), Lecture Notes in Computer Science (LNCS)
Original Kurzfassung:
Recently, it has been proposed to use approximation techniques
in the context of decision procedures for the quantifier-free theory
of fixed-size bit-vectors. We discuss existing and novel variants of underapproximation
techniques. Under-approximations produce smaller models
and may reduce solving time significantly. We propose a new technique
that allows early termination of an under-approximation refinement
loop, although the original formula is unsatisfiable. Moreover, we
show how over-approximation and under-approximation techniques can
be combined. Finally, we evaluate the effectiveness of our approach on
array and bit-vector benchmarks of the SMT library.