A Tutorial on Verifying LinkedList using KeY: Part 3c
The work
| Authors | Jinting Bian; Hans-Dieter A. Hiep |
|---|---|
| Editors | |
| Type | dataset |
| Year | 2020 |
| Also known as | bian2020tutorialb |
| Citekey | bian2020tutorialpart3c |
Where it appeared
| Published in | Figshare |
|---|---|
| Publisher | Figshare (United Kingdom) |
Identifiers
| DOI | 10.6084/m9.figshare.11688870 |
|---|---|
| OpenAlex | W6957870868 |
Access
| Landing page | https://figshare.com/articles/A_Tutorial_on_Verifying_LinkedList_using_KeY_Part_3c/11688870 |
|---|
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 unlink() 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 unlink() consists of 5 parts. This part shows the case in which one of the tests of the if-statements in unlink() evaluate to false; and the other evaluates to true.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-24 13:49 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{bian2020tutorialpart3c,
title = {A Tutorial on Verifying LinkedList using KeY: Part 3c},
author = {Jinting Bian and Hans-Dieter A. Hiep},
year = {2020},
journal = {Figshare},
publisher = {Figshare (United Kingdom)},
doi = {10.6084/m9.figshare.11688870},
}
This record lives at https://refs.drheap.org/bian2020tutorialpart3c/ and will keep
doing so. It used to be called bian2020tutorialb, and those addresses still resolve to this one.