KIT | KIT-Bibliothek | Impressum | Datenschutz

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

Stuber, Johanna

Abstract:

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. ... mehr

Abstract (englisch):

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. ... mehr


Volltext §
DOI: 10.5445/IR/1000162878
Veröffentlicht am 06.10.2023
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Informationssicherheit und Verlässlichkeit (KASTEL)
Publikationstyp Hochschulschrift
Publikationsdatum 11.09.2023
Sprache Englisch
Identifikator KITopen-ID: 1000162878
Verlag Karlsruher Institut für Technologie (KIT)
Umfang 66 S.
Art der Arbeit Abschlussarbeit - Bachelor
Prüfungsdaten 11.09.2023
Schlagwörter KeY, Java Modeling Language, deductive verification, red-black trees
Referent/Betreuer Beckert, Bernhard
Ulbrich, Mattias
Pfeifer, Wolfram
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page