SMArT // Satisfiability modulo Arithmetik und Theorien

• Antragsteller: Dr. Michael Sagraloff, seit 3/2016
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2013 bis 2018
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 242816019

Das Projektziel ist, fortgeschrittene Techniken zum arithmetischen Schließen für die formale Softwareverifikation bereitzustellen. Während des letzten Jahrzehnts gab es enorme Fortschritte bei der Softwareverifikation. Wesentlich war dabei die Entwicklung von SMT-Solvern, die erfolgreich angewendet wurden für Softwareverifikation, bounded und parametrisches Model-Checking, Generieren von Tests, usw. SMT-Solver kombinieren SAT-Solver mit Theorie-Solvern für das Entscheiden von Mengen von Literalen über interpretierten Symbolen und mit Instanziierungstechniken für Quantoren.Ein Grundproblem bei der Verifikation ist das Schließen in Fragmenten der Arithmetik. Arithmetik bezeichnet dabei Theorien, deren Sprache Funktionen 0, 1, +, *, optional auch mod, sin, exp usw. umfassen, interpretiert über ganzen, rationalen, reellen oder komplexen Zahlen, oder auch über Kombinationen dieser Bereiche. Zahlreiche bekannte Resultate zur Entscheidbarkeit und Komplexität von Fragmenten der Arithmetik zeigen klare Grenzen für automatische Tools auf. Für viele praktische Anwendungen genügt es jedoch, begrenzte Teilprobleme zu betrachten.Heutige SMT-Solver sind meist auf lineare Arithmetik beschränkt. Dies genügt zwar, um z. B. die Verletzung von Arraygrenzen in einfachen heapmanipulierenden Programmen auszuschließen, jedoch ist die Ausdrucksstärke stark einschränkt. Es gibt Ansätze stärkere Fragmente der Arithmetik zu unterstützen, deren Anwendbarkeit jedoch sehr beschränkt ist, da sie existierende Resultate und Systeme weitgehend ignorieren.Wir schlagen im Gegensatz dazu vor, existierende Techniken und Systeme an den SMT-Kontext anzupassen. Dies hat mehrere Vorteile: (1) Der arithmetische Solver muss sich nicht um die boolesche Struktur kümmern. (2) Der SMT-Solver erhält Zugriff auf die ausgereifte Infrastruktur des arithmetischen Solvers. (3) Der Anwender des Arithmetik-Solvers profitiert von der modularen Architektur des SMT-Solvers indem er die Arithmetik mit anderen Theorien kombinieren kann.Eine solche Integration erfordert grundlegende Erweiterungen auf der Arithmetikseite wie etwa die Erzeugung von Modellen oder unerfüllbaren Kernen. Umgekehrt muss man auf der SMT-Seite typische konzeptuelle Annahmen aufgeben: Die Theorien sind nicht mehr notwendigerweise konvex; falls etwa der lineare Spezialfall von einem eigenen Solver behandelt wird, sind sie auch nicht mehr disjunkt.Wir werde unsere Techniken in einem Solver implementieren, der Redlog, einen effizienten ausgereiften Solver für nichtlineare Arithmetik, kombiniert mit veriT, einem State-of-the-Art SMT-Solver. Dieses integrierte Produkt wird unter einer liberalen Open-Source-Lizenz zur Verfügung gestellt. Wir werden Benchmarkprobleme von Rodin und TLAPS und nichtlineare Probleme aus der SMT-LIB verwenden, um das Projekt zu evaluieren. Entwickler der erwähnten Softwareprodukte gehören zu den Antragstellern.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Frankreich
• Partnerorganisation: Agence Nationale de la Recherche / The French National Research Agency
• Beteiligte Person: Professor Dr. Pascal Fontaine
• Ehemaliger Antragsteller: Privatdozent Dr. Thomas Sturm, bis 3/2016