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

descriptionPublicationkeyboard_double_arrow_right Part of book or chapter of book , Article , Report , Conference object , Contribution for newspaper or weekly magazine , Book 01 Jan 2022 English Publisher:Springer International PublishingJournal:Formal Aspects of Computing, volume 35, pages 1-26 (issn: 0934-5043, eissn: 1433-299X,

Copyright policy )

Authors: Martin De Boer; Stijn De Gouw; Jonas Klamroth; Christian Jung; Mattias Ulbrich; Alexander Weigl;

doi: 10.1007/978-3-031-07727-2_4 , 10.1145/3594729 , 10.5445/ir/1000148092 , 10.5445/ir/1000145727

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

- Summary
- Subjects
- Related research
  (1)
- Metrics

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.

Related Organizations

Karlsruhe Institute of Technology
Germany
Karlsruhe Institute of Technology / KIT
Germany
Open University in the Netherlands
Netherlands
Research Center for Information Technology
Germany

Keywords

ddc:004, Data structures, Specification and verification (program logics, model checking, etc.), Verified Hash Map, cooperative verification, verified hash map, real-world case study, verified data structure, Real-world case study, Cooperative verification, Deductive program verification, Verified hash map, deductive program verification, Java modeling language, Verified data structure, Verified Data Structure, DATA processing & computer science, Theory of programming languages, Real-world case study \and, Deductive Program Verification, Cooperative Verification, 004, Java Modeling Language, info:eu-repo/classification/ddc/004

1 Research products, page 1 of 1

Application Of Java-Based Pointcuts In Aspect Oriented Programming (Aop) For Data Race Detection
2012IsAmongTopNSimilarDocuments

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	13
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Top 10%
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Top 10%