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

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 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
PublisherSpringer
Pages45-62
Number of pages18
Volume13274
ISBN (Electronic)978-3-031-07727-2
ISBN (Print)978-3-031-07726-5
DOIs
Publication statusPublished - 1 Jun 2022
Event17th International Conference on integrated Formal Methods - Lugano, Switzerland
Duration: 7 Jun 202210 Jun 2022
https://ifm22.si.usi.ch/

Publication series

SeriesLecture Notes in Computer Science

Conference

Conference17th International Conference on integrated Formal Methods
Abbreviated titleiFM 2022
Country/TerritorySwitzerland
CityLugano
Period7/06/2210/06/22
Internet address

Keywords

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

Fingerprint

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