@inbook{acc58f3e139541fba092d5b7c48e7f89,
title = "A Tutorial on Verifying LinkedList Using KeY",
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 {\textquoteleft}benchmark{\textquoteright} for specification and (automatic) verification techniques.",
keywords = "KeY, Linked list, Program correctness, Theorem proving",
author = "Hiep, {Hans-Dieter A.} and Jinting Bian and Boer, {Frank S. de} and Gouw, {Stijn de}",
note = "DBLP's bibliographic metadata records provided through http://dblp.org/search/publ/api are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.",
year = "2020",
doi = "10.1007/978-3-030-64354-6_9",
language = "English",
isbn = "978-3-030-64353-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "221--245",
editor = "Ahrendt, {Wolfgang } and Beckert, {Bernhard } and Bubel, {Richard } and H{\"a}hnle, {Reiner } and Ulbrich, {Mattias }",
booktitle = "Deductive Software Verification",
}