Richard Bubel
5 references under this name, matched as it is written. Somebody else may write under it too, and the same person may appear here spelled another way.
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
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.
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