Verifying OpenJDK's LinkedList using KeY
This work addresses the problem of ensuring correctness in widely-used software libraries for developers and users, but it is incremental as it applies existing verification methods to a specific case study.
The paper tackled the formal verification of a corrected version of Java's LinkedList implementation from the OpenJDK standard library, using the KeY tool and Java Modeling Language to specify and verify the code, resulting in a verified corrected implementation.
As a particular case study of the formal verification of state-of-the-art, real software, we discuss the specification and verification of a corrected version of the implementation of a linked list as provided by the Java Collection framework. Keywords: Java, standard library, deductive verification, KeY, Java Modeling Language, case study, bug