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.

Hans-Dieter A. Hiep

Hans-Dieter A. Hiep: KeY verification of shipped JDK code (OpenJDK LinkedList and BitSet, a real defect found), history-based reasoning about object invariants, and footprint/separation logic for OO programs.

History-based reasoning about behavioral subtyping (extended paper)

Jinting Bian and others (2026) · Theoretical Computer Science · Elsevier BV

History-Based Reasoning About Behavioral Subtyping

Jinting Bian and others (2024) · Theoretical Aspects of Computing · Springer

New Foundations for Separation Logic

Hans-Dieter A. Hiep (2024)

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

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

Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic

Frank S. de Boer and others (2021) · ACM Transactions on Programming Languages and Systems · Association for Computing Machinery

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