"Lambdas, Arrays and Quantifiers"
, Johannes Kepler University, 2-2017
Lambdas, Arrays and Quantifiers
Sprache des Titels:
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
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.