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
A grouping.
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.
33 references
History-based reasoning about behavioral subtyping (extended paper)
Jinting Bian and others (2026) · Theoretical Computer Science · Elsevier BV
The Critical State of Cyberspace
Hans-Dieter Hiep (2026) · Advances in Anti-Access and Area Denial (A2/AD): From Defensive Technologies to A Whole-of-Society Approach · Leiden University Press
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
New Foundations for Separation Logic (Coq artifact)
Hans-Dieter Hiep (2024) · Zenodo
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
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)