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.
Frank S. de Boer: what can be proved about object-oriented programs - WP-calculus, syntax-directed Hoare logic, completeness - and the same question asked of shipped code: OpenJDK sort, LinkedList and BitSet with KeY.
29 references
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
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
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
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
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
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 Sort Method for Generic Collections
Stijn de Gouw and others (2019) · Journal of Automated Reasoning · Springer
Verifying OpenJDK's LinkedList using KeY: Proof Files
Hans-Dieter A. Hiep and others (2019) · Figshare · Figshare (United Kingdom)
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
A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts
Cees Pierik and others (2003) · Formal Methods for Open Object-Based Distributed Systems · Springer
A WP-calculus for OO
Frank S. de Boer (1999) · Foundations of Software Science and Computation Structures · Springer
Reasoning about Dynamically Evolving Process Structures; a proof theory for the parallel object-oriented language pool
Frank S. de Boer (1991) · Vrije Universiteit Amsterdam