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.1145/3594729

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: Contribution to journal › Article › 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 article, 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
Article number	18
Number of pages	26
Journal	Formal Aspects of Computing
Volume	35
Issue number	3
DOIs	https://doi.org/10.1145/3594729
Publication status	Published - 13 Sept 2023

Access to Document

10.1145/3594729Licence: CC0

Cite this

@article{88c8e313b8b4435da5d8edc48296e5dd,

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

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

note = "DBLP's bibliographic metadata records provided through http://dblp.org/search/publ/api are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.",

year = "2023",

month = sep,

day = "13",

doi = "10.1145/3594729",

language = "English",

volume = "35",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "Springer London",

number = "3",

}

TY - JOUR

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

N1 - DBLP's bibliographic metadata records provided through http://dblp.org/search/publ/api are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.

PY - 2023/9/13

Y1 - 2023/9/13

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

U2 - 10.1145/3594729

DO - 10.1145/3594729

M3 - Article

SN - 0934-5043

VL - 35

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 3

M1 - 18

ER -

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

Abstract

Access to Document

Fingerprint

Cite this