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.
Jinting Bian
A grouping.
The most recent layer of the verifying-real-java work: verification of OpenJDK's LinkedList with KeY, abstract data types integrated into that method, and history-based reasoning about object invariants running to 2026. Two of the records are artefacts rather than papers -- a screencast and a Zenodo deposit of KeY proof files -- whose underlying article the corpus does not hold, which is open request 62. Several of the threads are held in more than one printing, so check which stage is meant before citing.
7 references
History-based reasoning about behavioral subtyping (extended paper)
Jinting Bian and others (2026) · Theoretical Computer Science · Elsevier BV
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