Kolloquiumsvortrag: Deduktive Verifikation von Java-Programmen mit KeY

Kurzfassung:
Für den Nachweis der funktionalen Korrektheit von Java-Programmen wird seit 25 Jahren in Karlsruhe KeY entwickelt. KeY ist ein interaktiver Theorembeweiser der auf einem Sequenzenkalkül für die Dynamische Logik aufbaut. Mithilfe von KeY wurde bereits ein Fehler in TimSort (Javas Standardalgorithmus für Sortierung) [de Gouw et. al., CAV'2015] gefunden, oder die Korrektheit der der `IdentityHashMap` [de Boer et.al., iFM'2022, Best Paper] gezeigt.