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 journalArticleAcademicpeer-review


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 languageEnglish
Article number18
Number of pages26
JournalFormal Aspects of Computing
Issue number3
Publication statusPublished - 13 Sept 2023


Dive into the research topics of 'Formal Specification and Verification of JDK's Identity Hash Map Implementation'. Together they form a unique fingerprint.

Cite this