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.
Deductive verification of production Java with KeY, applied to code that ships in the JDK rather than to examples: OpenJDK's LinkedList and BitSet are both taken through the tool and a real defect found. The other two threads are history-based reasoning about object invariants and, with de Boer and de Gouw, footprint and separation logic for object-oriented programs. dblp: https://dblp.org/pid/253/3994
11 references
History-based reasoning about behavioral subtyping (extended paper)
Jinting Bian and others (2026) · Theoretical Computer Science · Elsevier BV
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
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
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
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