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
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.
@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},
}