Verifying OpenJDK's LinkedList using KeY
Hans-Dieter A. Hiep, Olaf Maathuis, Jinting Bian, Frank S. de Boer,, Marko van Eekelen, Stijn de Gouw
TL;DR
This paper presents a formal verification case study of OpenJDK's LinkedList implementation using the KeY deductive verification tool, demonstrating the effectiveness of formal methods in verifying real-world software components.
Contribution
It introduces a formal specification and verification process for a Java LinkedList, showcasing how KeY can be applied to verify correctness of standard library code.
Findings
Verified the correctness of a corrected LinkedList implementation
Identified potential bugs in the original implementation
Demonstrated the applicability of formal methods to real-world Java code
Abstract
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
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsModel-Driven Software Engineering Techniques · Business Process Modeling and Analysis · Simulation Techniques and Applications