Verifying OpenJDK's LinkedList using KeY
The work
| Authors | Hans-Dieter A. Hiep; Olaf Maathuis; Jinting Bian; Frank S. de Boer; Marko van Eekelen; Stijn de Gouw |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2020 |
| Citekey | hiep2020verifying |
Where it appeared
| Published in | Tools and Algorithms for the Construction and Analysis of Systems |
|---|---|
| Publisher | Springer |
| Pages | 217--234 |
Identifiers
| arXiv | 1911.04195 |
|---|---|
| DOI | 10.1007/978-3-030-45237-7_13 |
| OpenAlex | W3009942802 |
Access
| Landing page | https://doi.org/10.1007/978-3-030-45237-7_13 |
|---|---|
| Free full text | https://link.springer.com/content/pdf/10.1007%2F978-3-030-45237-7_13.pdf |
Related
| Distinct from | hiep2020tutorial |
|---|---|
| Distinct from | hiep2022verifying |
| Distinct from | matthews2006verification |
Abstract
As a particular case study of the formal verification of state-of-the-art, real software, we discuss the specification and verification of a corrected version of the implementation of a linked list as provided by the Java Collection framework.
Cite it as
@inproceedings{hiep2020verifying,
title = {Verifying OpenJDK's LinkedList using KeY},
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 = {2020},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
publisher = {Springer},
pages = {217--234},
eprint = {1911.04195},
doi = {10.1007/978-3-030-45237-7_13},
}
This record lives at https://refs.drheap.org/hiep2020verifying/ and will keep doing so.