Aina Niemetz,
"Bit Precise Reasoning Beyond Bit-Blasting"
, Johannes Kepler University, 2-2017
Original Titel:
Bit Precise Reasoning Beyond Bit-Blasting
Sprache des Titels:
Englisch
Original Kurzfassung:
In the field of hardware and software verification, many applications require
to determine satisfiability of first-order-logic with respect to one or more background
theories, also referred to as Satisfiability Modulo Theories (SMT). The
majority of these applications relies on bit-precise reasoning as provided by SMT
solvers for the quantifier-free theory of fixed-size bit-vectors, often combined with
arrays and uninterpreted functions. Fixed-size bit-vectors provide a natural way
to model circuits and programs and arrays allow to reason about memory and
array data structures. Uninterpreted functions, on the other hand, are useful as
abstraction for irrelevant or too complex details of a system.
In this thesis, our main focus is on SMT procedures for bit-vector logics. In
the context of quantifier-free bit-vector formulas in SMT, current state-of-theart
is a flattening technique referred to as bit-blasting, where the input formula
is eagerly translated into propositional logic and handed to an underlying SAT
solver.
In the context of combining quantifier-free bit-vectors with arrays and uninterpreted
functions, current state-of-the-art SMT procedures are based on lazy
rather than eager techniques. One such lazy technique is the Lemmas on Demand
(LOD) approach, which refines full candidate models of a formula abstraction
with lemmas until convergence. Full candidate models, however, include irrelevant
parts of the input formula, which may introduce unnecessary overhead. In
this thesis, we propose an optimization of LOD where focusing refinement on
relevant parts of the input formula considerably improves performance.