Verifying OpenJDK's LinkedList using KeY (extended paper)

Hans-Dieter A. Hiep*, Olaf Maathuis, Jinting Bian, Frank S. de Boer, Stijn de Gouw

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review


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.

Original languageEnglish
Pages (from-to)783-802
Number of pages20
JournalInternational Journal on Software Tools for Technology Transfer
Issue number5
Publication statusPublished - Oct 2022


  • Bug
  • Case study
  • Deductive verification
  • Java Modeling Language
  • KeY
  • Standard library


Dive into the research topics of 'Verifying OpenJDK's LinkedList using KeY (extended paper)'. Together they form a unique fingerprint.

Cite this