Bit Precise Reasoning Beyond Bit-Blasting

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.