Verifying OpenJDK's LinkedList using KeY

The work

TitleVerifying OpenJDK's LinkedList using KeY
AuthorsHans-Dieter A. Hiep; Olaf Maathuis; Jinting Bian; Frank S. de Boer; Marko van Eekelen; Stijn de Gouw
Typeconference paper
Year2020
Citekeyhiep2020verifying

Where it appeared

Published inTools and Algorithms for the Construction and Analysis of Systems
PublisherSpringer
Pages217--234

Identifiers

DOI10.1007/978-3-030-45237-7_13
OpenAlexW3009942802

Access

Landing pagehttps://doi.org/10.1007/978-3-030-45237-7_13
Free full texthttps://link.springer.com/content/pdf/10.1007%2F978-3-030-45237-7_13.pdf

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.

Copy held

KindPDF, 325.7 kB
Retrieved2026-08-08
Heldlocal, for personal reference
Where it came fromhttps://link.springer.com/content/pdf/10.1007/978-3-030-45237-7_13.pdf?error=cookies_not_supported&code=a52a9633-bc53-41a0-ad40-d27d976233cd

Where this came from

How it got herethe agent went looking · found via openalex
First seen2026-08-04
Recordreviewed by a person
Approved2026-08-18
In: Lecture Notes in Computer Science series Tools and Algorithms for the Construction and Analysis of Systems (TACAS) venue Verifying real Java topic

Cite it as

@inproceedings{hiep2020verifying,
  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},
  year = {2020},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
  pages = {217--234},
  publisher = {Springer},
  doi = {10.1007/978-3-030-45237-7_13},
  url = {https://link.springer.com/content/pdf/10.1007%2F978-3-030-45237-7_13.pdf},
}

This record lives at https://refs.drheap.org/hiep2020verifying/ and will keep doing so.