A Tutorial on Verifying LinkedList using KeY: Part 3d
The work
| Authors | Jinting Bian; Hans-Dieter A. Hiep |
|---|---|
| Editors | |
| Type | dataset |
| Year | 2020 |
| Also known as | bian2020tutorialc |
| Citekey | bian2020tutorialpart3d |
Where it appeared
| Published in | Figshare |
|---|---|
| Publisher | Figshare (United Kingdom) |
Identifiers
| DOI | 10.6084/m9.figshare.11688984 |
|---|---|
| OpenAlex | W6976978293 |
Access
| Landing page | https://figshare.com/articles/A_Tutorial_on_Verifying_LinkedList_using_KeY_Part_3d/11688984 |
|---|
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 both of the tests of the if-statements in unlink() evaluate to false. Large part of the class invariant is proven. Furthermore, this part proves the class invariant property involving the prev field of the chain. The last part consists of proving the property involving the next field of the chain.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-24 13:51 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{bian2020tutorialpart3d,
title = {A Tutorial on Verifying LinkedList using KeY: Part 3d},
author = {Jinting Bian and Hans-Dieter A. Hiep},
year = {2020},
journal = {Figshare},
publisher = {Figshare (United Kingdom)},
doi = {10.6084/m9.figshare.11688984},
}
This record lives at https://refs.drheap.org/bian2020tutorialpart3d/ and will keep
doing so. It used to be called bian2020tutorialc, and those addresses still resolve to this one.