A Tutorial on Verifying LinkedList using KeY: Part 4a
The work
| Authors | Jinting Bian; Hans-Dieter A. Hiep |
|---|---|
| Editors | |
| Type | dataset |
| Year | 2020 |
| Also known as | bian2020tutoriald |
| Citekey | bian2020tutorialpart4a |
Where it appeared
| Published in | Figshare |
|---|---|
| Publisher | Figshare (United Kingdom) |
Identifiers
| DOI | 10.6084/m9.figshare.11699178 |
|---|---|
| OpenAlex | W6977429150 |
Access
| Landing page | https://figshare.com/articles/media/A_Tutorial_on_Verifying_LinkedList_using_KeY_Part_4a/11699178 |
|---|
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
In this proof session, we show part of how to prove the implementation of the remove() method of the java.util.LinkedList correct with respect to its method contract using the KeY prover. The method contract is specified using JML (not shown in video). The complete proof of remove() consists of 2 parts: this video shows the first part, the case where the argument is null.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-24 13:53 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{bian2020tutorialpart4a,
title = {A Tutorial on Verifying LinkedList using KeY: Part 4a},
author = {Jinting Bian and Hans-Dieter A. Hiep},
year = {2020},
journal = {Figshare},
publisher = {Figshare (United Kingdom)},
doi = {10.6084/m9.figshare.11699178},
}
This record lives at https://refs.drheap.org/bian2020tutorialpart4a/ and will keep
doing so. It used to be called bian2020tutoriald, and those addresses still resolve to this one.