Verifying OpenJDK's LinkedList using KeY
Logic in Computer Science
2019-11-12 v1 Software Engineering
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
Cite
@article{arxiv.1911.04195,
title = {Verifying OpenJDK's LinkedList using KeY},
author = {Hans-Dieter A. Hiep and Olaf Maathuis and Jinting Bian and Frank S. de Boer and Marko van Eekelen and Stijn de Gouw},
journal= {arXiv preprint arXiv:1911.04195},
year = {2019}
}
Comments
16 pages, 9 pages appendix