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.

Frank S. de Boer

A grouping.

What can be proved about an object-oriented program, and at what cost: a WP-calculus and syntax-directed Hoare logic for OO, then the completeness question that runs through the textbook on sequential and concurrent programs and on to reasoning about call-by-value. The second half asks the same question of code somebody actually runs -- the OpenJDK sorting defect found by proving the specification could not hold, and the LinkedList, abstract-data-type and history-based work that follows from it. A third strand approaches the same programs through what a component may touch, in footprint and dynamic separation logic.

History-based reasoning about behavioral subtyping (extended paper)

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

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

Symbolic execution formally explained

Frank S. de Boer and others (2021) · Formal Aspects of Computing

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

Verifying OpenJDK's Sort Method for Generic Collections

Stijn de Gouw and others (2019) · Journal of Automated Reasoning · Springer

Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

Stijn de Gouw and others (2016) · Software and Systems Modeling

Being and Change: Reasoning About Invariance

Frank S. de Boer and others (2015) · Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings

OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case

Stijn de Gouw and others (2015) · Computer Aided Verification · Springer

Proof Pearl: The KeY to Correct and Stable Sorting

Stijn de Gouw and others (2014) · Journal of Automated Reasoning · Springer

Formal Methods for Components and Objects, 10th International Symposium, FMCO 2011, Turin, Italy, October 3-5, 2011, Revised Selected Papers

Bernhard Beckert and others (2013) · Springer

Verification of object-oriented programs: A transformational approach

Krzysztof R. Apt and others (2012) · Journal of Computer and System Sciences

Abstract Object Creation in Dynamic Logic: To Be or Not to Be Created

Wolfgang Ahrendt and others (2009) · FM 2009: Formal Methods · Springer

Verification of Sequential and Concurrent Programs

Krzysztof R. Apt and others (2009) · Springer