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.

Jinting Bian: recent verifying-real-java work with KeY - OpenJDK LinkedList, ADTs in KeY, history-based invariant reasoning (to 2026). Two records are artefacts (a screencast, a Zenodo deposit); request 62 asks for their article.

28 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 (extended paper)
Frank S. de Boer and others (2025) · Formal Aspects of Computing · Association for Computing Machinery
History-Based Reasoning About Behavioral Subtyping
Jinting Bian and others (2024) · Theoretical Aspects of Computing · Springer
Reasoning about object-oriented programs: from classes to interfaces
Jinting Bian (2024)
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
Reasoning About Invariant Properties of Object-oriented Programs - dynamic frames: Proof files
Jinting Bian and others (2022) · Data Archiving and Networked Services (DANS) · Zenodo
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
Integrating ADTs in KeY and their Application to History-based Reasoning : Video Material
Jinting Bian and others (2021) · Data Archiving and Networked Services (DANS) · Royal Netherlands Academy of Arts and Sciences
Reasoning About Invariant Properties of Object-oriented Programs - dynamic frames
Jinting Bian and others (2021) · figshare
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
A Tutorial on Verifying LinkedList using KeY: Part 1
Jinting Bian and others (2020) · Figshare · Figshare (United Kingdom)
A Tutorial on Verifying LinkedList using KeY: Part 2
Jinting Bian and others (2020) · figshare
A Tutorial on Verifying LinkedList using KeY: Part 3a
Jinting Bian and others (2020) · figshare
A Tutorial on Verifying LinkedList using KeY: Part 3b
Jinting Bian and others (2020) · figshare
A Tutorial on Verifying LinkedList using KeY: Part 3c
Jinting Bian and others (2020) · Figshare · Figshare (United Kingdom)
A Tutorial on Verifying LinkedList using KeY: Part 3d
Jinting Bian and others (2020) · Figshare · Figshare (United Kingdom)
A Tutorial on Verifying LinkedList using KeY: Part 3e
Jinting Bian and others (2020) · figshare
A Tutorial on Verifying LinkedList using KeY: Part 4a
Jinting Bian and others (2020) · Figshare · Figshare (United Kingdom)
A Tutorial on Verifying LinkedList using KeY: Part 4b
Jinting Bian and others (2020) · figshare
A Tutorial on Verifying LinkedList using KeY: Video Material
Jinting Bian and others (2020) · Data Archiving and Networked Services (DANS) · Royal Netherlands Academy of Arts and Sciences
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 LinkedList using KeY: Proof Files
Hans-Dieter A. Hiep and others (2019) · Figshare · Figshare (United Kingdom)