Robert Brummayer,
"Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays"
, Universität Linz, 11-2009
Original Titel:
Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays
Sprache des Titels:
Englisch
Original Kurzfassung:
The Satisfiability Modulo Theories (SMT) problem is to decide the satisfiability
of a formula expressed in a (decidable) first-order background theory.
In this thesis we address the problem of designing, implementing, testing, and
debugging an efficient SMT solver for the quantifier-free extensional theory
of arrays, combined with bit-vectors. This thesis consists of three main parts.
After an introduction into the problem and its domain, the first part
considers the design of an efficient decision procedure for the quantifier-free
extensional theory of arrays. We discuss the decision procedure in detail. In
particular, we prove correctness, provide a complexity analysis, and discuss
implementation and optimization details.
The second part focuses on the design and implementation details of our
SMT solver, called Boolector. In the SMT competitions 2008 and 2009,
Boolector clearly won the division of the quantifier-free theory of bit-vectors,
arrays and uninterpreted functions QF AUFBV. Moreover, it won the division
of the quantifier-free theory of bit-vectors QF BV in 2008 and achieved the second
place in 2009. We discuss selected optimization techniques and features
such as symbolic overflow detection, propagating unconstrained variables,
and under-approximation techniques for bit-vectors.
In the last part, this thesis addresses engineering aspects such as testing
and debugging techniques optimized for SMT solver development. We show
that fuzzing and debugging techniques can be successfully applied to SMT
solvers. We report on critical defects, such as segmentation faults and incorrect
results, which we have found for state-of-the-art SMT solvers. Finally,
we demonstrate the effectiveness of delta-debugging techniques in minimizing
failure-inducing SMT formulas.
Forschungs-