Konferenzbeitrag
SMT-Solving, Interpolation und Quantoren
Vorschaubild nicht verfügbar
Volltext URI
Dokumententyp
Text/Conference Paper
Zusatzinformation
Datum
2023
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
Gesellschaft für Informatik e.V.
Zusammenfassung
Satisfiability Modulo Theories, kurz SMT, bezeichnet das Problem, ob eine Formel in einer sogenannten Theorie, die die erlaubten Symbole und deren Interpretation einschränkt, erfüllbar ist. SMT-Solver werden zum Beispiel in der Softwareverifikation, Testgenerierung oder Programmsynthese eingesetzt. In der hier zusammengefassten Dissertation [Sc22] werden verschiedene Methoden vorge- stellt, die Probleme im Bereich des SMT-Solving lösen. Zum einen wird eine Entscheidungsprozedur für die Arraytheorie mit Constant Arrays vorgestellt, welche sich zum Beispiel zur Modellierung von initialisiertem Speicher eignen. Darauf aufbauend wird eine Interpolationsmethode für diese Theorie entwickelt. Interpolanten werden beispielsweise eingesetzt, um in der Softwareverifikation Kandidaten für Schleifeninvarianten zu generieren. Zuletzt wird eine Instanziierungsmethode vorgestellt, um quantifizierte Probleme zu lösen, die zum Beispiel bei der Verifikation von Sortieralgorithmen auftreten. Alle vorgestellten Methoden sind im Open-Source SMT-Solver SMTInterpol implementiert.