Verification of Red-Black Trees in KeY - A Case Study in Deductive Java Verification

Während das ausführliche Testen von Software das Auftreten von Fehlern unwahrscheinlicher macht, kann mit formaler Verifikation durch Beweise garantiert werden, dass sich ein Programm für sämtliche Eingaben korrekt verhält. Besonders für tausendfach verwendete Grundelemente wie die Datenstrukturen und Algorithmen einer Standardbibliothek ist eine formale Verifikation daher erstrebenswert.
In dieser Fallstudie spezifizieren und verifizieren wir eine Java-Implementierung von Rot-Schwarz-Bäumen mit KeY. KeY ist ein Tool zur formalen Verifikation von Java-Programmen, und verwendet dabei Dynamic Frames für Aussagen über Speicherbereiche, also das Framing. ... mehrRot-Schwarz-Bäume sind eine beliebte Datenstruktur für das effiziente Speichern und Auslesen von Elementen und sind zum Beispiel in der Klasse java.util.TreeMap der Java Class Library umgesetzt. In beiden Bereichen existieren verschiedenste Fallstudien – die in KeY betrachten jedoch kaum Baumstrukturen und existierende Rot-Schwarz-Baum-Verifizierungen gehen auf andere Weise als KeY mit Framing um.
In dieser Arbeit kommen wir zu dem Schluss, dass die Verifikation von Baumstrukturen mit Dynamic Frames möglich ist, jedoch im Vergleich zu anderen Ansätzen viel zusätzlichen Aufwand mit sich bringt. Darüber hinaus erkunden wir generelle Stärken und Schwächen von KeY und machen einige Vorschläge zur Verbesserung der Benutzbarkeit. Außerdem testen wir mit JML Scripts und Proof Caching neue Methoden zur Beweis-Automatisierung und -Persistierung.

While thorough testing of software reduces the likelihood of errors, formal verification can guarantee the correct behaviour of programs for all inputs through proofs. Consequently, for the ubiquitous data structures and algorithms like those found in standard libraries, used by thousands of applications, formal verification is especially desirable.
In this case study, we specify and verify a Java implementation of red-black trees with KeY. The KeY system is a tool for the formal verification of Java programs, and uses dynamic frames for memory reasoning, that is, framing. ... mehrRed-black trees are a popular data structure for the efficient storage and retrieval of ordered elements, for example implemented in the class java.util.TreeMap of the Java Class Library. There exist various case studies in both areas – those in KeY, however, rarely consider tree structures, and existing red-black-tree verifications use different approaches to framing compared to KeY.
In this work, we conclude that successful reasoning over tree structures with dynamic frames is possible, yet very work-intensive compared to other framing approaches. Apart from this, we explore general strengths and limitations of KeY and give suggestions on how to improve its usability. Furthermore, we test out methods for automising and persisting proofs with the new KeY features of JML Scripts and Proof Caching.