Lambdas, Arrays and Quantifiers

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.