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. Six of these records verify parts of OpenJDK, and twice the attempt found a defect testing had not.
39 references
Analysis and Formal Specification of OpenJDK's BitSet
Andy S. Tatman et al. (2024) · Integrated Formal Methods
Verification of Red-Black Trees in KeY - A Case Study in Deductive Java Verification
Johanna Stuber (2023)
Verifying OpenJDK's LinkedList using KeY (extended paper)
Hans-Dieter A. Hiep et al. (2022) · International Journal on Software Tools for Technology Transfer
On Deductive Verification of an Industrial Concurrent Software Component with VerCors
Raúl E. Monti et al. (2022) · Leveraging Applications of Formal Methods, Verification and Validation
Permission-based verification of red-black trees and their merging
Lukas Armborst et al. (2021) · 2021 IEEE/ACM 9th International Conference on Formal Methods in Software Engineering (FormaliSE)
Integrating ADTs in KeY and their Application to History-based Reasoning
Jinting Bian et al. (2021) · 24th International Symposium on Formal Methods (FM)
Symbolic execution formally explained
Frank S. de Boer et al. (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
History-Based Specification and Verification of Java Collections in KeY
Hans-Dieter A. Hiep et al. (2020) · Integrated Formal Methods
Verifying OpenJDK's LinkedList using KeY
Hans-Dieter A. Hiep et al. (2020) · Tools and Algorithms for the Construction and Analysis of Systems
Verifying OpenJDK's Sort Method for Generic Collections
Stijn de Gouw et al. (2019) · Journal of Automated Reasoning
Experience Report on Formally Verifying Parts of OpenJDK's API with KeY
Alexander Knüppel et al. (2018) · Formal Integrated Development Environment 2018 (F-IDE 2018)
The VerCors Tool Set: Verification of Parallel and Concurrent Software
Stefan Blom et al. (2017) · Integrated Formal Methods
Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic
Stijn de Gouw et al. (2016) · Software and Systems Modeling
Deductive Software Verification – The KeY Book
Mattias Ulbrich et al. (2016)
Permission-based separation logic for multithreaded Java programs
Afshin Amighi et al. (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 et al. (2015) · Computer Aided Verification
A Fully Verified Container Library
Nadia Polikarpova et al. (2015) · FM 2015: Formal Methods
The VerCors tool for verification of concurrent programs
Stefan Blom et al. (2014) · International Symposium on Formal Methods
OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse
David R. Cok (2014) · Formal Integrated Development Environment 2014 (F-IDE 2014)
Proof Pearl: The KeY to Correct and Stable Sorting
Stijn de Gouw et al. (2014) · Journal of Automated Reasoning
Formal Specification with JML
Marieke Huisman et al. (2014)
JML Reference Manual
Gary T. Leavens et al. (2013)
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java
Bart Jacobs et al. (2011) · NASA Formal Methods
The 1st Verified Software Competition: Experience Report
Vladimir Klebanov et al. (2011) · FM 2011: Formal Methods
Dynamic frames in Java dynamic logic
Peter H. Schmitt et al. (2011) · International Conference on Formal Verification of Object-Oriented Software (FoVeOOS)
Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction
Benjamin Weiß (2011)
Abstract Object Creation in Dynamic Logic: To Be or Not to Be Created
Wolfgang Ahrendt et al. (2009) · FM 2009: Formal Methods
Ensuring the correctness of lightweight tactics for JavaCard dynamic logic
Richard Bubel et al. (2008) · Electronic Notes in Theoretical Computer Science
jStar: Towards Practical Verification for Java
Dino Distefano et al. (2008) · Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications
Full functional verification of linked data structures
Karen Zee et al. (2008) · ACM SIGPLAN Notices
Verification of object-oriented software: The KeY approach
Bernhard Beckert et al. (2007)
Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions
Ioannis T. Kassios (2006) · FM 2006: Formal Methods
A machine-checked model for a Java-like language, virtual machine, and compiler
Gerwin Klein et al. (2006) · ACM Transactions on Programming Languages and Systems
Local reasoning for Java
Matthew J. Parkinson (2005)
Taclets: A New Paradigm for Constructing Interactive Theorem Provers
Bernhard Beckert et al. (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 et al. (1999) · Behavioral Specifications of Businesses and Systems
Java_light is type-safe—definitely
Tobias Nipkow et al. (1998) · Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '98)