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.
Stijn de Gouw
A grouping.
Deductive verification of production Java with KeY, and the claim behind it: that proof finds defects in code already shipped and widely trusted, not only in code written to be verified. The result the work is built around is the demonstration that OpenJDK's sorting routine could not meet its specification, held here with the proof that preceded it and the completed verification that followed; the LinkedList and abstract-data-type verifications apply the same method again. Two records step outside to footprint and dynamic separation logic, approaching the same programs through what a component may touch. dblp: https://dblp.org/pid/34/11095
14 references
Analysis and Formal Specification of OpenJDK's BitSet
Andy S. Tatman and others (2024) · Integrated Formal Methods · Springer
Dynamic Separation Logic
Frank S. de Boer and others (2023) · 39th Conference on the Mathematical Foundations of Programming Semantics (MFPS) · Electronic Notes in Theoretical Informatics and Computer Science
Footprint Logic for Object-Oriented Components
Frank S. de Boer and others (2022) · Formal Aspects of Component Software · Springer International Publishing
Verifying OpenJDK's LinkedList using KeY (extended paper)
Hans-Dieter A. Hiep and others (2022) · International Journal on Software Tools for Technology Transfer · Springer
Integrating ADTs in KeY and their Application to History-based Reasoning
Jinting Bian and others (2021) · 24th International Symposium on Formal Methods (FM) · Springer
History-Based Specification and Verification of Java Collections in KeY
Hans-Dieter A. Hiep and others (2020) · Integrated Formal Methods · Springer
A Tutorial on Verifying LinkedList Using KeY
Hans-Dieter A. Hiep and others (2020) · Deductive Software Verification: Future Perspectives · Springer International Publishing
Verifying OpenJDK's LinkedList using KeY
Hans-Dieter A. Hiep and others (2020) · Tools and Algorithms for the Construction and Analysis of Systems · Springer
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
Being and Change: Reasoning About Invariance
Frank S. de Boer and others (2015) · Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings
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
Proof Pearl: The KeY to Correct and Stable Sorting
Stijn de Gouw and others (2014) · Journal of Automated Reasoning · Springer
Verification of object-oriented programs: A transformational approach
Krzysztof R. Apt and others (2012) · Journal of Computer and System Sciences