Verifying OpenJDK's LinkedList using KeY (extended paper)

The work

AuthorsHans-Dieter A. Hiep; Olaf Maathuis; Jinting Bian; Frank S. de Boer; Stijn de Gouw
Editors
Typearticle
Year2022
Citekeyhiep2022verifying

Where it appeared

Published inInternational Journal on Software Tools for Technology Transfer
PublisherSpringer
Volume24
Issue5
Pages783--802

Related

Distinct fromhiep2020tutorial
Distinct fromhiep2020verifying

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.

How it got here

How it got hereagent via bibtex
Added2026-08-05 00:00 UTC
Approved bya person 2026-08-16 22:18 UTC

Cite it as

@article{hiep2022verifying,
  title        = {Verifying OpenJDK's LinkedList using KeY (extended paper)},
  author       = {Hans-Dieter A. Hiep and Olaf Maathuis and Jinting Bian and Frank S. de Boer and Stijn de Gouw},
  year         = {2022},
  journal      = {International Journal on Software Tools for Technology Transfer},
  publisher    = {Springer},
  volume       = {24},
  number       = {5},
  pages        = {783--802},
  doi          = {10.1007/s10009-022-00679-7},
}

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