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

Abstract

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
PublisherSpringer
Pages221-245
Number of pages25
ISBN (Electronic)978-3-030-64354-6
ISBN (Print)978-3-030-64353-9
DOIs
Publication statusPublished - 2020

Publication series

SeriesLecture Notes in Computer Science
Volume12345
ISSN0302-9743

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

Cite this