This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Reiner Hähnle
A grouping.
The KeY line: the deductive verification system for Java that most of verifying-real-java depends on, held as the taclet rule mechanism and the two book-length accounts a decade apart, with two of the OpenJDK results the tool made possible -- the paper showing the shipped sorting routine broken, and the completed verification. The sixth record, 'Dijkstra's legacy on program verification', is an assessment of what came of the Dijkstra material the corpus also holds.
6 references
Dijkstra's legacy on program verification
Reiner Hähnle (2022) · Edsger Wybe Dijkstra: His Life, Work, and Legacy · Association for Computing Machinery
Verifying OpenJDK's Sort Method for Generic Collections
Stijn de Gouw and others (2019) · Journal of Automated Reasoning · Springer
Deductive Software Verification – The KeY Book
Mattias Ulbrich and others (2016) · Springer
OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case
Stijn de Gouw and others (2015) · Computer Aided Verification · Springer
Verification of object-oriented software: The KeY approach
Bernhard Beckert and others (2007) · Springer-Verlag
Taclets: A New Paradigm for Constructing Interactive Theorem Provers
Bernhard Beckert and others (2004) · RACSAM