Transferring proof obligations from program verification in KeY to Isabelle/HOL

Korrektheitsgarantien für Programme werden heutzutage immer wichtiger. KeY ist ein System, das genutzt werden kann, um die formale Korrektheit von Java Programmen zu zeigen. Es nutzt syntaktische Ersetzungsregeln, genannt taclets, um Beweise sukzessive zu vereinfachen. Diese taclet Regeln können in KeY von einem automatisierten Beweismodus angewandt werden. Weil die Automatisierung nicht ausreichend ist, um manche Beweise zu schließen, und, weil Beweise Tausende von Regelanwendungen enthalten können, ist es wünschenswert, dem Nutzer stärkere automatisierte Werkzeuge bereitzustellen. ... mehrEin solches Werkzeug ist die Satisfiability Modulo Theories (SMT) Übersetzung von KeY, die es erlaubt SMT Beweiser zu nutzen, um Beweise zu schließen. Auch der SMT-Übersetzung fehlt es für manche Beweise an Regeln oder Beweisstärke. Es ist daher trotzdem wünschenswert, die bereits vorhandenen automatisierten Werkzeuge, die KeY Nutzer zur Verfügung haben, zu erweitern.
Diese Arbeit entwirft eine Übersetzung von KeY Beweisen zum generischen Beweisassistenten Isabelle/HOL, der auf Logik höherer Ordnung aufbaut. Zusätzlich zum Entwerfen dieser Übersetzung zeigt diese Arbeit auch, dass die Übersetzung automatisiert und in KeY integriert werden kann, indem die Übersetzung als eine GUI-Extension für KeY implementiert wird.
Diese Arbeit testet die entwickelte Isabelle Übersetzung auf über 2 400 Beweiszielen aus KeY Beispielen. Dadurch zeigte sich, dass die Isabelle Übersetzung einen Vorteil gegenüber der SMT Übersetzung und der KeY Automatik bietet. Obwohl die Isabelle Übersetzung nicht in der Lage ist, alle Beweise zu schließen, die die KeY Automatik oder die SMT Übersetzung schließen konnten, war sie dennoch in der Lage, Ziele zu schließen, die die KeY Automatik oder die SMT Übersetzung nicht schließen konnten. Daher ergänzt die Isabelle Übersetzung die automatisierten Werkzeuge des KeY Nutzers auf sinnvolle Weise, und schafft gleichzeitig eine Grundlage dafür, Isabelle in KeY auf andere Weise als zur automatischen Beweisführung zu nutzen.

Guarantees of correctness of programs are becoming more and more important nowadays. KeY is one tool, which can be used to prove the formal correctness of Java programs. It uses syntactic rewriting rules, called taclets, to successively simplify proofs. These taclet rules can be applied by an automated proving mode in KeY. Because the automation can be insufficient for closing some proofs and because proofs can contain thousands of rule applications, it is desirable to provide stronger automated tools to the user. One such tool is the Satisfiablity Modulo Theories (SMT) translation of KeY, which allows the use of SMT provers to close proofs. ... mehrThe SMT translation also lacks the required rules or proving strength for some proofs. It is thus still desirable to improve the already present automated toolset of KeY users.
This work designs a translation of KeY proofs to the higher-order logic prover Isabelle/HOL. In addition to designing this translation this work also shows that the translation can be automated and integrated within KeY by implementing it as a GUI extension of KeY.
This work tests the developed Isabelle translation on over 2 400 example proof obligations of KeY. In doing so the Isabelle translation has been found to offer some advantages over the SMT translation and the KeY automation. Although the Isabelle translation does not manage to close all proofs the KeY automation or SMT translation could close, it is able to close proofs, which the KeY automation or the SMT translation could not close. Thus the Isabelle translation expands the KeY user's automated toolset in a meaningful way, while also building a foundation for using Isabelle in ways outside automated proof solving in KeY.