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. 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.Das "Satisfiability Modulo Theories (SMT)" Problem beschäftigt sich mit der Erfüllbarkeit von Formeln in Prädikatenlogik erster Stufe unter Berücksichtigung einer oder mehrerer Theorien. In vielen Anwendungen im Bereich der Hardware und Software Verifikation werden SMT Prozeduren (auch SMT Solver genannt) als Backend verwendet um komplexe Verifikationsprobleme zu lösen, die üblicherweise mehrere Theorien kombinieren, wie z.B. die Theorie der Bitvektoren mit der Theorie der Arrays. Diese Dissertation beschäftigt sich mit Entscheidungsprozeduren für die Theorie der Arrays kombiniert mit nicht-interpretierten Funktionen und für Bitvektoren in Kombination mit Quantoren. Wir stellen eine Entscheidungsprozedur für nicht-rekursive, nicht-extensionale Lambdaterme erster Stufe vor, welche in unserem SMT Solver Boolector für die Theorie der Arrays kombiniert mit nicht-interpretierten Funktionen zum Einsatz kommt. Wir beschreiben unterschiedliche Implementierungsaspekte und Algorithmen und diskutieren die Vorteile von Lambdatermen in Bezug auf die Darstellung von Arrays. Zusätzlich stellen wir eine Erweiterung für unsere Entscheidungsprozedur vor, die uns ermöglicht mit Gleichheit von Arrays, die als Lambdaterme dargestellt werden, umzugehen und beschreiben eine Optimierung, die im Allgemeinen die Laufzeit von Boolector verbessert. Weiters beschäftigen wir uns mit unterschiedlichen Array Strukturen, die in existierenden SMT Benchmarks zum Einsatz kommen und die mit Lambdatermen kompakter dargestellt werden können. Wir zeigen, dass die alternative Darstellungsform mit Lambdatermen die Erzeugung von besseren und stärkeren Lemmas in unserer Entscheidungsprozedur ermöglicht. Dies hat zur Folge, dass die Performanz besonders auf Benchmarks, die durch symbolische Programmausführung erzeugt wurden, wesentlich gesteigert werden kann. Im letzten Teil dieser Dissertation beschäftigten wir uns mit einem neuen Ansatz zum Lösen von quantifizierten SMT Problemen mit Fokus auf quantifizierten Bitvektoren. Unser Ansatz kombiniert eine Technik namens "counterexample-guided quantifier instantiation" mit einer Technik aus dem Bereich der Synthese um Interpretationen für Skolemfunktionen und Terme für die Instantiierung von Quantoren zu synthetisieren. Unsere Ergebnisse zeigen, dass unser Ansatz zum Lösen von quantifizierten Bitvektoren im Vergleich zum aktuellen Stand der Technik kompetitiv ist. Weiters beschreiben wir eine Erweiterung und einige Optimierung für unseren neuen Ansatz, der im Allgemeinen die Performanz wesentlich verbessert.eingereicht von Dipl.-Ing. Mathias Preiner, BscUniversität Linz, Dissertation, 2017OeBB(VLID)191538