Verifying OpenJDK’s LinkedList using KeY (extended paper)

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.

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2022-10, Vol.24 (5), p.783-802
Main Authors: Hiep, Hans-Dieter A., Maathuis, Olaf, Bian, Jinting, de Boer, Frank S., de Gouw, Stijn
Format: Article
Language:English
Subjects:
Case studies
Computer Science
Java
Libraries
Semantics
Software
Software Engineering
Software Engineering/Programming and Operating Systems
Theory of Computation
Verification
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1433-2779
1433-2787
DOI:10.1007/s10009-022-00679-7