A Tutorial on Verifying LinkedList Using KeY

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review


This is a tutorial paper on using KeY to demonstrate formal verification of state-of-the-art, real software. In sufficient detail for a beginning user of JML and KeY, the specification and verification of part of a corrected version of the java.util.LinkedList class of the Java Collection framework is explained. The paper includes video material that shows recordings of interactive sessions, and project files with solutions. As such, this material is also interesting for the expert user and the developer of KeY as a ‘benchmark’ for specification and (automatic) verification techniques.
Original languageEnglish
Title of host publicationDeductive Software Verification
Subtitle of host publicationFuture Perspectives
EditorsWolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Mattias Ulbrich
Place of PublicationCham
Number of pages25
ISBN (Electronic)978-3-030-64354-6
ISBN (Print)978-3-030-64353-9
Publication statusPublished - 2020

Publication series

SeriesLecture Notes in Computer Science


  • KeY
  • Linked list
  • Program correctness
  • Theorem proving


Dive into the research topics of 'A Tutorial on Verifying LinkedList Using KeY'. Together they form a unique fingerprint.

Cite this