Verifying OpenJDK's LinkedList using KeY: Proof Files
The work
| Authors | Hans-Dieter A. Hiep; Olaf Maathuis; Jinting Bian; Frank S. de Boer; Marko van Eekelen; Stijn de Gouw |
|---|---|
| Editors | |
| Type | misc |
| Year | 2019 |
| Also known as | hiep2019verifying |
| Citekey | hiep2019verifyingproof |
Where it appeared
| Published in | Figshare |
|---|---|
| Publisher | Figshare (United Kingdom) |
Identifiers
| DOI | 10.5281/zenodo.3517081 |
|---|---|
| OpenAlex | W6931148476 |
Access
| Landing page | https://figshare.com/articles/Verifying_OpenJDK_s_LinkedList_using_KeY_Proof_Files/11500692 |
|---|
Related
| Superseded by | hiep2021verifyingproof |
|---|
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 archive contains a formal specification of Java's linked list. The archive contains an annotated version of java.util.LinkedList using the Java Modeling Language. Additionally, it includes the KeY version used to formally verify the annotated methods, and the corresponding proof files. The OpenJDK8 version can be found here: https://hg.openjdk.java.net/jdk8/jdk8/jdk/file/687fd7c7986d/src/share/classes/java/util/LinkedList.java
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-25 00:22 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{hiep2019verifyingproof,
title = {Verifying OpenJDK's LinkedList using KeY: Proof Files},
author = {Hans-Dieter A. Hiep and Olaf Maathuis and Jinting Bian and Frank S. de Boer and Marko van Eekelen and Stijn de Gouw},
year = {2019},
journal = {Figshare},
publisher = {Figshare (United Kingdom)},
doi = {10.5281/zenodo.3517081},
}
This record lives at https://refs.drheap.org/hiep2019verifyingproof/ and will keep
doing so. It used to be called hiep2019verifying, and those addresses still resolve to this one.