Verifying OpenJDK's LinkedList using KeY

Hans-Dieter A. Hiep; Olaf Maathuis; Jinting Bian; Frank S. de Boer; Marko C. J. D. van Eekelen; Stijn de Gouw

doi:10.1007/978-3-030-45237-7_13

Verifying OpenJDK's LinkedList using KeY

Hans-Dieter A. Hiep^*, Olaf Maathuis, Jinting Bian, Frank S. de Boer, Marko C. J. D. van Eekelen, Stijn de Gouw

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › 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
Title of host publication	TACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software
Editors	Armin Biere, David Parker
Place of Publication	Cham
Publisher	Springer
Pages	217-234
Number of pages	18
ISBN (Electronic)	978-3-030-45237-7
ISBN (Print)	978-3-030-45236-0
DOIs	https://doi.org/10.1007/978-3-030-45237-7_13
Publication status	Published - 17 Apr 2020
Event	(Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Dublin, Ireland Duration: 25 Apr 2020 → 30 Apr 2020 Conference number: 26 https://etaps.org/2020/tacas https://link.springer.com/content/pdf/10.1007%2F978-3-030-45237-7.pdf

Publication series

Series	Lecture Notes in Computer Science
Volume	12079
ISSN	0302-9743

Series	Theoretical Computer Science and General Issues (LNCS subseries)
Volume	12079

Conference

Conference	(Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Abbreviated title	TACAS 2020
Country/Territory	Ireland
City	Dublin
Period	25/04/20 → 30/04/20
Internet address	https://etaps.org/2020/tacas https://link.springer.com/content/pdf/10.1007%2F978-3-030-45237-7.pdf

Keywords

Java Modeling Language
Java standard library
KeY
bug
case study
deductive verification

Access to Document

10.1007/978-3-030-45237-7_13Licence: CC BY

Cite this

Hiep, H.-D. A., Maathuis, O., Bian, J., Boer, F. S. D., Eekelen, M. C. J. D. V., & Gouw, S. D. (2020). Verifying OpenJDK's LinkedList using KeY. In A. Biere, & D. Parker (Eds.), TACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems : 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software (pp. 217-234). Springer. https://doi.org/10.1007/978-3-030-45237-7_13

Hiep, Hans-Dieter A. ; Maathuis, Olaf ; Bian, Jinting et al. / Verifying OpenJDK's LinkedList using KeY. TACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems : 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software. editor / Armin Biere ; David Parker. Cham : Springer, 2020. pp. 217-234 (Lecture Notes in Computer Science, Vol. 12079). (Theoretical Computer Science and General Issues (LNCS subseries), Vol. 12079).

@inproceedings{1c6b05864dbd45b4af131112432576f3,

title = "Verifying OpenJDK's LinkedList using KeY",

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 = "Java Modeling Language, Java standard library, KeY, bug, case study, deductive verification",

author = "Hiep, {Hans-Dieter A.} and Olaf Maathuis and Jinting Bian and Boer, {Frank S. de} and Eekelen, {Marko C. J. D. van} and Gouw, {Stijn de}",

year = "2020",

month = apr,

day = "17",

doi = "10.1007/978-3-030-45237-7_13",

language = "English",

isbn = "978-3-030-45236-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "217--234",

editor = "Armin Biere and David Parker",

booktitle = "TACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems",

note = "(Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020 ; Conference date: 25-04-2020 Through 30-04-2020",

url = "https://etaps.org/2020/tacas, https://link.springer.com/content/pdf/10.1007%2F978-3-030-45237-7.pdf",

}

Hiep, H-DA, Maathuis, O, Bian, J, Boer, FSD, Eekelen, MCJDV & Gouw, SD 2020, Verifying OpenJDK's LinkedList using KeY. in A Biere & D Parker (eds), TACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems : 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software. Springer, Cham, Lecture Notes in Computer Science, vol. 12079, Theoretical Computer Science and General Issues (LNCS subseries), vol. 12079, pp. 217-234, (Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Dublin, Ireland, 25/04/20. https://doi.org/10.1007/978-3-030-45237-7_13

Verifying OpenJDK's LinkedList using KeY. / Hiep, Hans-Dieter A.; Maathuis, Olaf; Bian, Jinting et al.
TACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems : 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software. ed. / Armin Biere; David Parker. Cham: Springer, 2020. p. 217-234 (Lecture Notes in Computer Science, Vol. 12079). (Theoretical Computer Science and General Issues (LNCS subseries), Vol. 12079).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Verifying OpenJDK's LinkedList using KeY

AU - Hiep, Hans-Dieter A.

AU - Maathuis, Olaf

AU - Bian, Jinting

AU - Boer, Frank S. de

AU - Eekelen, Marko C. J. D. van

AU - Gouw, Stijn de

N1 - Conference code: 26

PY - 2020/4/17

Y1 - 2020/4/17

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 - Java Modeling Language

KW - Java standard library

KW - KeY

KW - bug

KW - case study

KW - deductive verification

U2 - 10.1007/978-3-030-45237-7_13

DO - 10.1007/978-3-030-45237-7_13

M3 - Conference Article in proceeding

SN - 978-3-030-45236-0

T3 - Lecture Notes in Computer Science

SP - 217

EP - 234

BT - TACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems

A2 - Biere, Armin

A2 - Parker, David

PB - Springer

CY - Cham

T2 - (Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

Y2 - 25 April 2020 through 30 April 2020

ER -

Hiep HDA, Maathuis O, Bian J, Boer FSD, Eekelen MCJDV, Gouw SD. Verifying OpenJDK's LinkedList using KeY. In Biere A, Parker D, editors, TACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems : 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software. Cham: Springer. 2020. p. 217-234. (Lecture Notes in Computer Science, Vol. 12079). (Theoretical Computer Science and General Issues (LNCS subseries), Vol. 12079). doi: 10.1007/978-3-030-45237-7_13

Verifying OpenJDK's LinkedList using KeY

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this