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 language | English |
---|---|
Title of host publication | Integrated Formal Methods - 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings |
Editors | Maurice H. ter Beek, Rosemary Monahan |
Place of Publication | Cham |
Publisher | Springer |
Pages | 45-62 |
Number of pages | 18 |
Volume | 13274 |
ISBN (Electronic) | 978-3-031-07727-2 |
ISBN (Print) | 978-3-031-07726-5 |
DOIs | |
Publication status | Published - 1 Jun 2022 |
Event | 17th International Conference on integrated Formal Methods - Lugano, Switzerland Duration: 7 Jun 2022 → 10 Jun 2022 https://ifm22.si.usi.ch/ |
Publication series
Series | Lecture Notes in Computer Science |
---|
Conference
Conference | 17th International Conference on integrated Formal Methods |
---|---|
Abbreviated title | iFM 2022 |
Country/Territory | Switzerland |
City | Lugano |
Period | 7/06/22 → 10/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.Prizes
-
Best paper award iFM 2022
de Gouw, S. (Recipient), 2022
Prize: Prize (including medals and awards) › Academic
Student theses
-
Formal analysis of the Java Collections Framework
de Boer, M. (Author), de Gouw, S. (Examiner) & Vos, T. (Co-assessor), 23 Jul 2021Student thesis: Master's Thesis
File