Verifying OpenJDK's LinkedList using KeY (extended paper)

Hans-Dieter A. Hiep; Olaf Maathuis; Jinting Bian; Frank S. de Boer; Stijn de Gouw

doi:10.1007/s10009-022-00679-7

Verifying OpenJDK's LinkedList using KeY (extended paper)

Hans-Dieter A. Hiep^*, Olaf Maathuis, Jinting Bian, Frank S. de Boer, Stijn de Gouw

^*Corresponding author for this work

Research output: Contribution to journal › Article › Academic › peer-review

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.

Original language	English
Pages (from-to)	783-802
Number of pages	20
Journal	International Journal on Software Tools for Technology Transfer
Volume	24
Issue number	5
DOIs	https://doi.org/10.1007/s10009-022-00679-7
Publication status	Published - Oct 2022

Keywords

Bug
Case study
Deductive verification
Java Modeling Language
KeY
Standard library

Access to Document

10.1007/s10009-022-00679-7Licence: CC BY

Cite this

@article{f9120f87823e480196cac3cb59163366,

title = "Verifying OpenJDK's LinkedList using KeY (extended paper)",

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.",

keywords = "Bug, Case study, Deductive verification, Java Modeling Language, KeY, Standard library",

author = "Hiep, {Hans-Dieter A.} and Olaf Maathuis and Jinting Bian and Boer, {Frank S. de} and Gouw, {Stijn de}",

year = "2022",

month = oct,

doi = "10.1007/s10009-022-00679-7",

language = "English",

volume = "24",

pages = "783--802",

journal = "International Journal on Software Tools for Technology Transfer",

issn = "1433-2787",

publisher = "Springer Verlag",

number = "5",

}

TY - JOUR

T1 - Verifying OpenJDK's LinkedList using KeY (extended paper)

AU - Hiep, Hans-Dieter A.

AU - Maathuis, Olaf

AU - Bian, Jinting

AU - Boer, Frank S. de

AU - Gouw, Stijn de

PY - 2022/10

Y1 - 2022/10

N2 - 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.

AB - 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.

KW - Bug

KW - Case study

KW - Deductive verification

KW - Java Modeling Language

KW - KeY

KW - Standard library

U2 - 10.1007/s10009-022-00679-7

DO - 10.1007/s10009-022-00679-7

M3 - Article

SN - 1433-2787

VL - 24

SP - 783

EP - 802

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

IS - 5

ER -

Verifying OpenJDK's LinkedList using KeY (extended paper)

Abstract

Keywords

Access to Document

Fingerprint

Cite this