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

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.

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