Satisfiability Modulo Theories (SMT) refers to the problem of deciding the satisfiability of a first-order formula with respect to one or more first-order theories. In many applications of hardware and software verification, SMT solvers are employed as back-end engine to solve complex verification tasks that usually combine multiple theories, such as the theory of fixed-size bit-vectors and the theory of arrays. This thesis presents several advances in the design and implementation of theory solvers for the theory of arrays, uninterpreted functions and quantified bit-vectors.
We introduce a decision procedure for non-recursive non-extensional first-order lambda terms, which is implemented in our SMT solver Boolector to handle the theory of arrays and uninterpreted functions. We discuss various implementation aspects and algorithms as well as the advantage of using lambda terms for array reasoning. We provide an extension of the lemmas on demand for lambdas approach to handle extensional arrays and discuss an optimization that improves the overall performance of Boolector.
We further investigate common array patterns in existing SMT benchmarks that can be represented by means of more compact and succinct lambda terms. We show that exploiting lambda terms for certain array patterns is beneficial for lemma generation since it allows us to produce stronger and more succinct lemmas, which improve the overall performance, particularly on instances from symbolic execution. Our results suggest that a more expressive theory of arrays might be desirable for users of SMT solvers in order to allow more succinct encodings of common array operations.
We further propose a new approach for solving quantified SMT problems, with a particular focus on the theory of fixed-size bit-vectors. Our approach combines counterexample-guided quantifier instantiation with a syntax-guided synthesis approach to synthesize interpretations for Skolem functions and terms for quantifier instantiations. We discuss a simple yet effective approach that does not rely on heuristic quantifier instantiation techniques, which are commonly employed by current state-of-the-art SMT procedures for handling quantified formulas. We show that our techniques are competitive compared to the state-of-the-art in solving quantified bit-vectors and discuss extensions and optimizations that improve the overall performance of our approach.