Schindler, TanjaReischuk, Rüdiger2023-11-092023-11-092023978-3-88579-981-8https://dl.gi.de/handle/20.500.12116/42603Satisfiability 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.deText/Conference Paper