A Tutorial on Verifying LinkedList Using KeY
The work
| Authors | Hans-Dieter A. Hiep; Jinting Bian; Frank S. de Boer; Stijn de Gouw |
|---|---|
| Editors | |
| Type | incollection |
| Year | 2020 |
| Citekey | hiep2020tutorial |
Where it appeared
| Published in | Deductive Software Verification: Future Perspectives |
|---|---|
| Publisher | Springer International Publishing |
| Series | Lecture Notes in Computer Science |
| Pages | 221--245 |
Identifiers
| DOI | 10.1007/978-3-030-64354-6_9 |
|---|---|
| OpenAlex | W3105876241 |
Access
| Landing page | https://doi.org/10.1007/978-3-030-64354-6_9 |
|---|---|
| Free full text | https://ir.cwi.nl/pub/29986/29986.pdf |
Related
| Distinct from | hiep2020verifying |
|---|---|
| Distinct from | hiep2022verifying |
Abstract
This is a tutorial paper on using KeY to demonstrate formal verification of state-of-the-art, real software. In sufficient detail for a beginning user of JML and KeY, the specification and verification of part of a corrected version of the java.util.LinkedList class of the Java Collection framework is explained. The paper includes video material that shows recordings of interactive sessions, and project files with solutions. As such, this material is also interesting for the expert user and the developer of KeY as a 'benchmark' for specification and (automatic) verification techniques.
Cite it as
@incollection{hiep2020tutorial,
title = {A Tutorial on Verifying LinkedList Using KeY},
author = {Hans-Dieter A. Hiep and Jinting Bian and Frank S. de Boer and Stijn de Gouw},
year = {2020},
booktitle = {Deductive Software Verification: Future Perspectives},
publisher = {Springer International Publishing},
series = {Lecture Notes in Computer Science},
pages = {221--245},
doi = {10.1007/978-3-030-64354-6_9},
}
This record lives at https://refs.drheap.org/hiep2020tutorial/ and will keep doing so.