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

Stijn de Gouw: deductive verification of production Java with KeY, built around showing OpenJDK's sort could not meet its specification, with the proof before and the verified fix after, plus the LinkedList and ADT work.

Footprint Logic for Object-Oriented Components (extended paper)

Frank S. de Boer and others (2025) · Formal Aspects of Computing · Association for Computing Machinery

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

Integrating ADTs in KeY and their application to history-based reasoning about collection

Jinting Bian and others (2022) · Formal Methods in System Design · Springer Science and Business Media LLC

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

Integrating ADTs in KeY and their Application to History-based Reasoning: Proof Files

Jinting Bian and others (2021) · Zenodo

Verifying OpenJDK's LinkedList using KeY (Extended Paper): Proof Files

Hans-Dieter A. Hiep and others (2021) · Zenodo (CERN European Organization for Nuclear Research) · European Organization for Nuclear Research

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

A Tutorial on Verifying LinkedList using KeY: Proof Files

Hans-Dieter A. Hiep and others (2020) · Data Archiving and Networked Services (DANS) · Royal Netherlands Academy of Arts and Sciences

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

Verifying OpenJDK's LinkedList using KeY: Proof Files

Hans-Dieter A. Hiep and others (2019) · Figshare · Figshare (United Kingdom)

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