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 proceedingConference Article in proceedingAcademicpeer-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 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 languageEnglish
Title of host publicationIntegrated Formal Methods - 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings
EditorsMaurice H. ter Beek, Rosemary Monahan
Place of PublicationCham
Number of pages18
ISBN (Electronic)978-3-031-07727-2
ISBN (Print)978-3-031-07726-5
Publication statusPublished - 1 Jun 2022
Event17th International Conference on integrated Formal Methods - Lugano, Switzerland
Duration: 7 Jun 202210 Jun 2022

Publication series

SeriesLecture Notes in Computer Science


Conference17th International Conference on integrated Formal Methods
Abbreviated titleiFM 2022
Internet address


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


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