Test-of-Time Award für Professor Ralf Jung

?ber das Paper

Das Paper stellt Iris vor, ein vereinheitlichendes Framework f¨¹r nebenl?ufige Trennungslogik h?herer Ordnung, das im Rocq Prover (ehemals Coq) mechanisiert ist. Zu der Zeit, als Iris entstand, war das Feld der Trennungslogik gespalten, mit vielen unterschiedlichen und potenziell inkompatiblen Logiken, die mit massgeschneiderten Modellen entwickelt wurden. Diese erste Arbeit ¨¹ber Iris zeigte, wie einige Schl¨¹sselkomponenten aus fr¨¹heren Arbeiten ¨C insbesondere partielle kommutative Monoide zur Darstellung von benutzerdefinierten Geisterzust?nden (inspiriert durch das Views-Framework) und impredikative Invarianten h?herer Ordnung (inspiriert durch schrittweise indizierte Modelle) ¨C auf fruchtbare Weise kombiniert werden k?nnen, um eine Vielzahl anspruchsvoller Beweistechniken (wie z. B. ?logisch atomare Tripel¡°) abzuleiten, die in fr¨¹heren Logiken als primitiv eingebaut waren. Es war nur der erste Schritt in einer langen Reihe von Arbeiten einer reichen und vielf?ltigen Gemeinschaft von Iris-Entwickler*innen aus aller Welt. Dank der anschliessenden Arbeiten am Iris Proof Mode in Rocq ist Iris zu einem weit verbreiteten Werkzeug sowohl in der Programmuntersuchung als auch in der Metatheorie von Programmiersprachen geworden, mit Anwendungen, die von funktionalen Korrektheitsnachweisen f¨¹r Low-Level-Systemcode (z. B. Hypervisoren, absturzsichere Systeme, schwache Speicher-Datenstrukturen) bis hin zu erweiterbaren semantischen Soundness-Nachweisen f¨¹r High-Level-Systeme (z. B. Rust, OCaml, Scala) reichen.