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.
Verifying real Java
A subject the papers are about. The loosest grouping, and the one to reach for last.
Proving things about code people actually run. Collects deductive verification applied to production Java, chiefly OpenJDK library code, together with the specification and tooling work it requires. Membership requires the target to be shipped code rather than an example written to be verified.
41 references
History-based reasoning about behavioral subtyping (extended paper)
Jinting Bian and others (2026) · Theoretical Computer Science · Elsevier BV
Analysis and Formal Specification of OpenJDK's BitSet
Andy S. Tatman and others (2024) · Integrated Formal Methods · Springer
Verification of Red-Black Trees in KeY - A Case Study in Deductive Java Verification
Johanna Stuber (2023) · Karlsruhe Institute of Technology
Verifying OpenJDK's LinkedList using KeY (extended paper)
Hans-Dieter A. Hiep and others (2022) · International Journal on Software Tools for Technology Transfer · Springer
On Deductive Verification of an Industrial Concurrent Software Component with VerCors
Raúl E. Monti and others (2022) · Leveraging Applications of Formal Methods, Verification and Validation · Springer
Permission-based verification of red-black trees and their merging
Lukas Armborst and others (2021) · 2021 IEEE/ACM 9th International Conference on Formal Methods in Software Engineering (FormaliSE) · IEEE
Integrating ADTs in KeY and their Application to History-based Reasoning
Jinting Bian and others (2021) · 24th International Symposium on Formal Methods (FM) · Springer
Symbolic execution formally explained
Frank S. de Boer and others (2021) · Formal Aspects of Computing
JML and OpenJML for Java 16
David R. Cok (2021) · Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs · 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
Verifying OpenJDK's Sort Method for Generic Collections
Stijn de Gouw and others (2019) · Journal of Automated Reasoning · Springer
Experience Report on Formally Verifying Parts of OpenJDK's API with KeY
Alexander Knüppel and others (2018) · Formal Integrated Development Environment 2018 (F-IDE 2018) · Open Publishing Association
The VerCors Tool Set: Verification of Parallel and Concurrent Software
Stefan Blom and others (2017) · Integrated Formal Methods · Springer
Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic
Stijn de Gouw and others (2016) · Software and Systems Modeling
Deductive Software Verification – The KeY Book
Mattias Ulbrich and others (2016) · Springer
Permission-based separation logic for multithreaded Java programs
Afshin Amighi and others (2015) · Logical Methods in Computer Science
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
A Fully Verified Container Library
Nadia Polikarpova and others (2015) · FM 2015: Formal Methods · Springer
The VerCors tool for verification of concurrent programs
Stefan Blom and others (2014) · International Symposium on Formal Methods · Springer
OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse
David R. Cok (2014) · Formal Integrated Development Environment 2014 (F-IDE 2014) · Open Publishing Association
Proof Pearl: The KeY to Correct and Stable Sorting
Stijn de Gouw and others (2014) · Journal of Automated Reasoning · Springer
Formal Specification with JML
Marieke Huisman and others (2014) · Karlsruhe Institute of Technology
JML Reference Manual
Gary T. Leavens and others (2013)
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java
Bart Jacobs and others (2011) · NASA Formal Methods · Springer
The 1st Verified Software Competition: Experience Report
Vladimir Klebanov and others (2011) · FM 2011: Formal Methods · Springer
Dynamic frames in Java dynamic logic
Peter H. Schmitt and others (2011) · International Conference on Formal Verification of Object-Oriented Software (FoVeOOS) · Springer
Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction
Benjamin Weiß (2011) · Karlsruhe Institute of Technology
Abstract Object Creation in Dynamic Logic: To Be or Not to Be Created
Wolfgang Ahrendt and others (2009) · FM 2009: Formal Methods · Springer
Ensuring the correctness of lightweight tactics for JavaCard dynamic logic
Richard Bubel and others (2008) · Electronic Notes in Theoretical Computer Science
jStar: Towards Practical Verification for Java
Dino Distefano and others (2008) · Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications · Association for Computing Machinery
Full functional verification of linked data structures
Karen Zee and others (2008) · ACM SIGPLAN Notices · Association for Computing Machinery
Verification of object-oriented software: The KeY approach
Bernhard Beckert and others (2007) · Springer-Verlag
Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions
Ioannis T. Kassios (2006) · FM 2006: Formal Methods · Springer
A machine-checked model for a Java-like language, virtual machine, and compiler
Gerwin Klein and others (2006) · ACM Transactions on Programming Languages and Systems · Association for Computing Machinery
Local reasoning for Java
Matthew J. Parkinson (2005) · University of Cambridge, Computer Laboratory
Taclets: A New Paradigm for Constructing Interactive Theorem Provers
Bernhard Beckert and others (2004) · RACSAM
Taclets and the KeY prover
Martin Giese (2004) · Electronic Notes in Theoretical Computer Science
JML: A Notation for Detailed Design
Gary T. Leavens and others (1999) · Behavioral Specifications of Businesses and Systems · Springer US
Java_light is type-safe—definitely
Tobias Nipkow and others (1998) · Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '98) · Association for Computing Machinery