The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.

A Tutorial on Verifying LinkedList using KeY: Proof Files

The work

AuthorsHans-Dieter A. Hiep; Jinting Bian; Frank S. de Boer; Stijn de Gouw
Editors
Typemisc
Year2020
Also known ashiep2020tutorialb
Citekeyhiep2020tutorialproof

Where it appeared

Published inData Archiving and Networked Services (DANS)
PublisherRoyal Netherlands Academy of Arts and Sciences

Identifiers

DOI10.5281/zenodo.3613711
OpenAlexW6949911925

Access

Landing pagehttps://ir.cwi.nl/pub/29997

From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.

Abstract

The project files for the article `A Tutorial on Verifying LinkedList using KeY'. The archive contains: A bundled version of KeY, version 2.6.3. This requires a recent version of Java Runtime Edition (JRE) to be executed, say OpenJDK8. A number of stub contracts (jre/ directory). A skeleton LinkedList source file (src/java/util/LinkedList.old) for the reader of the tutorial to fill in the methods and contracts. The LinkedList source file after all modifications have been done (src/java/util/LinkedList.java) A number of proof files that can be loaded in KeY, that verify the correctness of the methods with respect to their contract as given in the solution.

How it got here

How it got hereagent via openalex
Added2026-10-24 13:55 UTC
Not denied bya person 2026-10-29 17:12 UTC

Cite it as

@misc{hiep2020tutorialproof,
  title        = {A Tutorial on Verifying LinkedList using KeY: Proof Files},
  author       = {Hans-Dieter A. Hiep and Jinting Bian and Frank S. de Boer and Stijn de Gouw},
  year         = {2020},
  journal      = {Data Archiving and Networked Services (DANS)},
  publisher    = {Royal Netherlands Academy of Arts and Sciences},
  doi          = {10.5281/zenodo.3613711},
}

This record lives at https://refs.drheap.org/hiep2020tutorialproof/ and will keep doing so. It used to be called hiep2020tutorialb, and those addresses still resolve to this one.