A Tutorial on Verifying LinkedList using KeY: Video Material
The work
| Authors | Jinting Bian; Hans-Dieter A. Hiep |
|---|---|
| Editors | |
| Type | misc |
| Year | 2020 |
| Also known as | bian2020tutoriale |
| Citekey | bian2020tutorialvideo |
Where it appeared
| Published in | Data Archiving and Networked Services (DANS) |
|---|---|
| Publisher | Royal Netherlands Academy of Arts and Sciences |
Identifiers
| DOI | 10.6084/m9.figshare.c.4826589 |
|---|---|
| OpenAlex | W6958885628 |
Access
| Landing page | https://ir.cwi.nl/pub/29998 |
|---|
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
This collection of video material consists of screen recordings of interactive proof sessions with the KeY theorem prover. Each video displays how to create a proof for part of one method contract, or proofs of several method contracts. The method contracts are expressed in the Java Modeling Language with KeY-specific extensions (not shown in the video).
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-24 13:54 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{bian2020tutorialvideo,
title = {A Tutorial on Verifying LinkedList using KeY: Video Material},
author = {Jinting Bian and Hans-Dieter A. Hiep},
year = {2020},
journal = {Data Archiving and Networked Services (DANS)},
publisher = {Royal Netherlands Academy of Arts and Sciences},
doi = {10.6084/m9.figshare.c.4826589},
}
This record lives at https://refs.drheap.org/bian2020tutorialvideo/ and will keep
doing so. It used to be called bian2020tutoriale, and those addresses still resolve to this one.