Formal Specification and Verification of JDK's Identity Hash Map Implementation

Martin de Boer; Stijn de Gouw; Jonas Klamroth; Christian Jung; Mattias Ulbrich; Alexander Weigl

doi:10.1007/978-3-031-07727-2_4

Formal Specification and Verification of JDK's Identity Hash Map Implementation

Martin de Boer, Stijn de Gouw, Jonas Klamroth, Christian Jung, Mattias Ulbrich, Alexander Weigl

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

Abstract

Hash maps are a common and important data structure in efficient algorithm implementations. Despite their wide-spread use, real-world implementations are not regularly verified. In this paper, we present the first case study of the IdentityHashMap class in the Java JDK. We specified its behavior using the Java Modeling Language (JML) and proved correctness for the main insertion and lookup methods with KeY, a semi-interactive theorem prover for JML-annotated Java programs. Furthermore, we report how unit testing and bounded model checking can be leveraged to find a suitable specification more quickly. We also investigated where the bottlenecks in the verification of hash maps lie for KeY by comparing required automatic proof effort for different hash map implementations and draw conclusions for the choice of hash map implementations regarding their verifiability.

Original language	English
Title of host publication	Integrated Formal Methods - 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings
Editors	Maurice H. ter Beek, Rosemary Monahan
Place of Publication	Cham
Publisher	Springer
Pages	45-62
Number of pages	18
Volume	13274
ISBN (Electronic)	978-3-031-07727-2
ISBN (Print)	978-3-031-07726-5
DOIs	https://doi.org/10.1007/978-3-031-07727-2_4
Publication status	Published - 1 Jun 2022
Event	17th International Conference on integrated Formal Methods - Lugano, Switzerland Duration: 7 Jun 2022 → 10 Jun 2022 https://ifm22.si.usi.ch/

Publication series

Series	Lecture Notes in Computer Science

Conference

Conference	17th International Conference on integrated Formal Methods
Abbreviated title	iFM 2022
Country/Territory	Switzerland
City	Lugano
Period	7/06/22 → 10/06/22
Internet address	https://ifm22.si.usi.ch/

Keywords

Cooperative verification
Deductive program verification
Java Modeling Language
Real-world case study
Verified data structure
Verified hash map

Access to Document

10.1007/978-3-031-07727-2_4

Best paper award iFM 2022
de Gouw, Stijn (Recipient), 2022
Prize: Prize (including medals and awards) › Academic

Formal analysis of the Java Collections Framework
Author: de Boer, M., 23 Jul 2021
Supervisor: de Gouw, S. (Examiner) & Vos, T. (Co-assessor)
Student thesis: Master's Thesis

File

Cite this

Boer, M. D., Gouw, S. D., Klamroth, J., Jung, C., Ulbrich, M., & Weigl, A. (2022). Formal Specification and Verification of JDK's Identity Hash Map Implementation. In M. H. T. Beek, & R. Monahan (Eds.), Integrated Formal Methods - 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings (Vol. 13274, pp. 45-62). Springer. https://doi.org/10.1007/978-3-031-07727-2_4

Boer, Martin de ; Gouw, Stijn de ; Klamroth, Jonas et al. / Formal Specification and Verification of JDK's Identity Hash Map Implementation. Integrated Formal Methods - 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings. editor / Maurice H. ter Beek ; Rosemary Monahan. Vol. 13274 Cham : Springer, 2022. pp. 45-62 (Lecture Notes in Computer Science).

@inproceedings{d9e94631474941889bd13b2525e19165,

title = "Formal Specification and Verification of JDK's Identity Hash Map Implementation",

abstract = "Hash maps are a common and important data structure in efficient algorithm implementations. Despite their wide-spread use, real-world implementations are not regularly verified. In this paper, we present the first case study of the IdentityHashMap class in the Java JDK. We specified its behavior using the Java Modeling Language (JML) and proved correctness for the main insertion and lookup methods with KeY, a semi-interactive theorem prover for JML-annotated Java programs. Furthermore, we report how unit testing and bounded model checking can be leveraged to find a suitable specification more quickly. We also investigated where the bottlenecks in the verification of hash maps lie for KeY by comparing required automatic proof effort for different hash map implementations and draw conclusions for the choice of hash map implementations regarding their verifiability.",

keywords = "Cooperative verification, Deductive program verification, Java Modeling Language, Real-world case study, Verified data structure, Verified hash map",

author = "Boer, {Martin de} and Gouw, {Stijn de} and Jonas Klamroth and Christian Jung and Mattias Ulbrich and Alexander Weigl",

year = "2022",

month = jun,

day = "1",

doi = "10.1007/978-3-031-07727-2_4",

language = "English",

isbn = "978-3-031-07726-5",

volume = "13274",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "45--62",

editor = "Beek, {Maurice H. ter} and Rosemary Monahan",

booktitle = "Integrated Formal Methods - 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings",

note = "17th International Conference on integrated Formal Methods, iFM 2022 ; Conference date: 07-06-2022 Through 10-06-2022",

url = "https://ifm22.si.usi.ch/",

}

Boer, MD, Gouw, SD, Klamroth, J, Jung, C, Ulbrich, M & Weigl, A 2022, Formal Specification and Verification of JDK's Identity Hash Map Implementation. in MHT Beek & R Monahan (eds), Integrated Formal Methods - 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings. vol. 13274, Springer, Cham, Lecture Notes in Computer Science, pp. 45-62, 17th International Conference on integrated Formal Methods, Lugano, Switzerland, 7/06/22. https://doi.org/10.1007/978-3-031-07727-2_4

Formal Specification and Verification of JDK's Identity Hash Map Implementation. / Boer, Martin de; Gouw, Stijn de; Klamroth, Jonas et al.
Integrated Formal Methods - 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings. ed. / Maurice H. ter Beek; Rosemary Monahan. Vol. 13274 Cham: Springer, 2022. p. 45-62 (Lecture Notes in Computer Science).

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

TY - GEN

T1 - Formal Specification and Verification of JDK's Identity Hash Map Implementation

AU - Boer, Martin de

AU - Gouw, Stijn de

AU - Klamroth, Jonas

AU - Jung, Christian

AU - Ulbrich, Mattias

AU - Weigl, Alexander

PY - 2022/6/1

Y1 - 2022/6/1

N2 - Hash maps are a common and important data structure in efficient algorithm implementations. Despite their wide-spread use, real-world implementations are not regularly verified. In this paper, we present the first case study of the IdentityHashMap class in the Java JDK. We specified its behavior using the Java Modeling Language (JML) and proved correctness for the main insertion and lookup methods with KeY, a semi-interactive theorem prover for JML-annotated Java programs. Furthermore, we report how unit testing and bounded model checking can be leveraged to find a suitable specification more quickly. We also investigated where the bottlenecks in the verification of hash maps lie for KeY by comparing required automatic proof effort for different hash map implementations and draw conclusions for the choice of hash map implementations regarding their verifiability.

AB - Hash maps are a common and important data structure in efficient algorithm implementations. Despite their wide-spread use, real-world implementations are not regularly verified. In this paper, we present the first case study of the IdentityHashMap class in the Java JDK. We specified its behavior using the Java Modeling Language (JML) and proved correctness for the main insertion and lookup methods with KeY, a semi-interactive theorem prover for JML-annotated Java programs. Furthermore, we report how unit testing and bounded model checking can be leveraged to find a suitable specification more quickly. We also investigated where the bottlenecks in the verification of hash maps lie for KeY by comparing required automatic proof effort for different hash map implementations and draw conclusions for the choice of hash map implementations regarding their verifiability.

KW - Cooperative verification

KW - Deductive program verification

KW - Java Modeling Language

KW - Real-world case study

KW - Verified data structure

KW - Verified hash map

U2 - 10.1007/978-3-031-07727-2_4

DO - 10.1007/978-3-031-07727-2_4

M3 - Conference Article in proceeding

SN - 978-3-031-07726-5

VL - 13274

T3 - Lecture Notes in Computer Science

SP - 45

EP - 62

BT - Integrated Formal Methods - 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings

A2 - Beek, Maurice H. ter

A2 - Monahan, Rosemary

PB - Springer

CY - Cham

T2 - 17th International Conference on integrated Formal Methods

Y2 - 7 June 2022 through 10 June 2022

ER -

Boer MD, Gouw SD, Klamroth J, Jung C, Ulbrich M, Weigl A. Formal Specification and Verification of JDK's Identity Hash Map Implementation. In Beek MHT, Monahan R, editors, Integrated Formal Methods - 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings. Vol. 13274. Cham: Springer. 2022. p. 45-62. (Lecture Notes in Computer Science). doi: 10.1007/978-3-031-07727-2_4

Formal Specification and Verification of JDK's Identity Hash Map Implementation

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Prizes

Best paper award iFM 2022

Student theses

Formal analysis of the Java Collections Framework

Cite this