SMT solving, interpolation, and quantifiers

Abstract: This thesis presents new methods in the area of satisfiability modulo theories (SMT). SMT solving has a wide range of applications, e.g., in software verification, test generation, or program synthesis. Besides deciding the satisfiability of quantifier-free or quantified formulas, tasks for SMT solvers include generating models for satisfiable formulas, proofs for unsatisfiable formulas, or interpolants.

In software verification, the theory of arrays is useful to encode constraints about array data structures or memory. Constant arrays, that contain only a single element at all positions, thereby provide a convenient way to model, e.g., initialization. We present a new decision procedure for the theory of arrays with constant arrays. Our work extends an existing decision procedure that exploits write chains between arrays to discover equalities between arrays or array elements, which requires new rules in the presence of constant arrays. The decision procedure only creates new lemmas when a current candidate model is conflicting with the theory of arrays, and therefore fits well in the standard DPLL(T ) framework.

Building on this decision procedure, we present a new interpolation procedure for the theory of arrays with constant arrays. Interpolants can be used in software verification to derive candidate invariants that help to prove the correctness of a program. Our interpolation procedure is integrated into a proof-based interpolation procedure that inductively computes the interpolant along the structure of the proof, and we provide the algorithms for the lemmas of the theory of arrays. These algorithms can efficiently use write chains between arrays to compute the interpolants. Nevertheless, the interpolants have exponential size and we show that this bound is optimal.

Finally, quantified formulas are required for instance when proving the correctness of a sorting algorithm. A typical approach in SMT solvers to deal with quantified formulas is to search for a model for the ground part of the formula and then successively add instances of the quantified formulas in order to refute the candidate model. We present a new instantiation-based method to solve quantified formulas in SMT that aims at choosing only such instances that are in conflict with a candidate model or that allow to propagate a literal. To this end, it uses E-matching, which is usually used in a heuristic instantiation method, and in our method provides both candidate instances and a means to evaluate them without building them.

All presented methods were implemented and evaluated in our open-source SMT solver SMTInterpol
Abstract: Diese Arbeit stellt neue Methoden vor, die sich mit dem Problem “Satisfiability modulo Theories” (SMT), der Erfüllbarkeit logischer Formeln in einer logischen Theorie, befassen.

SMT-Solving findet Anwendung im Bereich der Softwareverifikation, der Testgenerierung, oder der Programmsynthese. Neben einer Antwort auf die Frage, ob eine quantorenfreie oder auch eine quantifizierte Formel erfüllbar ist, können SMT-Solver auch Modelle für erfüllbare Formeln, Beweise für unerfüllbare Formeln oder sogenannte Interpolanten liefern.

In der Softwareverifikation wird die Arraytheorie eingesetzt, um in logischen Formeln Speicher oder Array-Datenstrukturen darzustellen. Sogenannte Constant Arrays, die an jeder Stelle dasselbe Element enthalten, können dabei zum Beispiel initialisierten Speicher modellieren. Wir stellen eine neue Entscheidungsprozedur für die Arraytheorie mit Constant Arrays vor. Dazu erweitern wir eine existierende Entscheidungsprozedur, die Ketten von Schreibvorgängen zwischen Arrays nutzt, um Gleichheiten zwischen Arrays oder den enthaltenen Elementen zu finden. Dafür bedarf es neuer Regeln für die Constant Arrays. Die Entscheidungsprozedur erzeugt nur dann neue Lemmas, wenn ein potentielles Modell der Formel in der Arraytheorie zum Konflikt führt. Dadurch eignet sich die Prozedur für die Integration in das in SMT-Solvern übliche DPLL(T )- Framework.

Aufbauend auf diese Entscheidungsprozedur stellen wir eine neue Interpolationsmethode für die Arraytheorie mit Constant Arrays vor. Interpolanten werden in der Softwareverifikation eingesetzt, um Invarianten herzuleiten, die benötigt werden, um die Korrektheit eines Programms zu zeigen. Die vorgestellte Interpolationsmethode baut auf einer beweisbasierten Methode auf, die Interpolanten induktiv über die Struktur des Beweises berechnet. Wir stellen die Algorithmen vor, die sogenannte partielle Interpolanten für Lemmas der Arraytheorie berechnen. Diese Algorithmen nutzen Schreibketten zwischen Arrays, um effizient Interpolanten berechnen zu können. Dennoch sind die berechneten Interpolanten exponentiell in der Größe der Lemmas, diese Schranke ist jedoch optimal.

Quantifizierte Formeln werden in der Softwareverifikation gebraucht, um beispielsweise die Korrektheit eines Sortieralgorithmus zu beweisen. Ein typischer Ansatz in SMT-Solvern ist es, für den quantorenfreien Teil der Formel ein Modell zu suchen, und nach und nach Instanzen der quantifizierten Formeln hinzuzufügen, die dieses Modell widerlegen. Wir stellen eine neue Instanziierungsmethode vor, deren Ziel es ist, nur solche Instanzen zu erzeugen, die direkt im Konflikt mit einem potentiellen Modell stehen, oder die es erlauben, neue Fakten zu propagieren. Zu diesem Zweck nutzen wir E-Matching, das üblicherweise als Basis von heuristischen Instanziierungsmethoden verwendet wird. In unserer Methode ermöglicht uns das E-Matching, nicht nur potentielle Instanzen zu finden, sondern sie auch auszuwerten, ohne sie erst erzeugen zu müssen.

Die vorgestellten Methoden wurden im Open Source SMT-Solver SMTInterpol integriert und ausgewertet

Angaben zum Objekt

• Standort: Deutsche Nationalbibliothek Frankfurt am Main
• Umfang: Online-Ressource
• Sprache: Englisch
• Anmerkungen: Universität Freiburg, Dissertation, 2022

Klassifikation und Themen

• Schlagwort: Automatisches Beweisverfahren ; Erfüllbarkeitsproblem ; Mathematische Logik ; Formale Methode ; Verifikation ; SMT Solver ; Erfüllbarkeitsproblem ; Model Checking

Beteiligte, Orts- und Zeitangaben

• Ereignis: Veröffentlichung
• (wo): Freiburg
• (wer): Universität
• (wann): 2022
• Urheber: Schindler, Tanja
• Beteiligte Personen und Organisationen: Podelski, Andreas ; Albert-Ludwigs-Universität Freiburg. Fakultät für Angewandte Wissenschaften

Weitere Informationen

• DOI: 10.6094/UNIFR/229572
• URN: urn:nbn:de:bsz:25-freidok-2295721
• Rechteinformation: Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
• Letzte Aktualisierung: 25.03.2025, 13:43 MEZ