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.
Richard Bubel
A grouping.
The join between the KeY system and the results got with it: the soundness of the prover's own rules for JavaCard dynamic logic, the KeY book itself, and three records of the OpenJDK work -- the paper showing the shipped sorting routine broken, the integration of deductive verification with symbolic execution, and the completed verification.
5 references
Verifying OpenJDK's Sort Method for Generic Collections
Stijn de Gouw and others (2019) · Journal of Automated Reasoning · Springer
Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic
Stijn de Gouw and others (2016) · Software and Systems Modeling
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
Ensuring the correctness of lightweight tactics for JavaCard dynamic logic
Richard Bubel and others (2008) · Electronic Notes in Theoretical Computer Science