Quantifizierte Formeln in interpolierenden SMT Solver

• Antragsteller: Dr. Jochen Hoenicke
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2015 bis 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 282631393

Ziel dieses Projektes ist es, die theoretischen und praktischen Grundlagen für einen interpolantenerzeugenden SMT-Solver für quantifizierte Formeln zu entwickeln. Dieses Ziel ist dadurch motiviert, dass in Software-Model-Checkern Interpolation verwendet wird. Genauer gesagt werden interpolantenerzeugende SMT-Solver erfolgreich in Software-Model-Checkern eingesetzt, um Kandidaten für Schleifeninvarianten zu erzeugen. Dies wird dadurch bekräftigt, dass mehrere Software-Model-Checker in der SV-COMP, einem internationalen Software-Verifikations-Wettbewerb, Interpolation benutzen. Ein Ergebnis des Projekts wird sein, dass die Klasse von Programmen, für die quantifizierte Zusicherungen benötigt werden, von jenen Software-Model-Checkern, die Interpolation benutzen, behandelt werden kann. Diese Klasse von Programmen ist praktisch relevant.Quantifizierte Zusicherungen werden beispielsweise benötigt, um zu spezifizieren, dass ein Array sortiert ist, oder dass jedes Element einer Hashmap eine Dateninvariante erfüllt.Wir werden das Ziel erreichen, indem wir den allgemeinen Ansatz aus der ersten Projektphase weiterverfolgen, und auf den technischen Erkenntnissen und Ergebnissen aus der ersten Projektphase aufbauen. Ein Herausstellungsmerkmal unseres Ansatzes ist, dass unser SMT-Solver von Anfang an auf die Erzeugung von Interpolanten ausgelegt ist und trotzdem als Solver wettbewerbsfähig ist.

• DFG-Verfahren: Sachbeihilfen