Reconstructing Z3 Proofs With KeY

KeY dient zur formalen Verifikation spezifizierter Eigenschaften von Java-Programmen.Dafür werden aus der formalen Spezifikation sowie dem Programm-Code Beweisverpflichtungen generiert. Diese werden dann Schritt für Schritt in eine Menge von Formeln der Prädikatenlogik erster Stufe überführt. Da diese allerdings unentscheidbar ist, ist es eine große Herausforderung, einen Beweis für diese Formelmenge zu finden.
Moderne SMT-Solver, wie zum Beispiel Z3, sind genau auf diesen Anwendungszweck hin optimiert. Daher ist schon lange in KeY die Möglichkeit eingebaut, (Teil-)Probleme für SMT-Solver zu übersetzen. ... mehrDas Ergebnis bei diesem Vorgehen ist ein partieller Beweis in KeY, der von (möglicherweise mehreren) SMT-Antworten komplettiert wird. Da Z3 aber auch Beweise für seine Antworten liefern kann, gibt es hier Verbesserungspotential: In dieser Thesis wird eine Technik zum Nachspielen der Z3 Beweise in KeY vorgestellt, sodass man als Ergebnis einen geschlossenen Beweis in KeY erhält und die SMT-Antworten verworfen werden können. Herausforderungen sowohl systematischer als auch technischer
Natur werden identifiziert and Lösungen dafür vogestellt.
Schließlich wird auch eine prototypische Implementierung der Technik zum Nachspielen der Beweise zur Verfügung gestellt. Im Evaluations-Teil der Arbeit wird die Leistungsfähigkeit dieser Implementierung sowie die zukünfigen Möglichkeiten erörtert.

KeY is a tool for formal verification of specified properties of Java programs. It works by generating proof obligations from formal specification and source code, and transforming it into a set of first-order formulas afterwards. Due to the undecidability of first-order logic it is a challenging problem to find a proof for this set of formulas.
Modern SMT solvers, such as Z3, provide highly optimized algorithms for exactly this purpose. Therefore, translating (sub-)problems to SMT solvers has long been possible from KeY. This approach resulted in a partial proof in KeY complemented by (possibly multiple) SMT results. ... mehrSince Z3 is able to produce proofs for its result, it is possible to improve upon this: This thesis presents a replay technique that allows for reconstruction of the proofs generated by Z3, such that the result is a closed proof in KeY and the SMT results can be dropped. Systematic as well as engineering challenges are identified and solutions for them presented.
A prototypical implementation of the replay technique in KeY is provided. In the evaluation part of this work, its capabilities as well as future potential is shown.