Formal Specification and Verification of JDK’s Identity Hash Map Implementation
Boer, Martin de; Gouw, Stijn de; Klamroth, Jonas 1; Jung, Christian 2; Ulbrich, Mattias
2,3; Weigl, Alexander
2,3
1 FZI Forschungszentrum Informatik (FZI)
2 Karlsruher Institut für Technologie (KIT)
3 Institut für Informationssicherheit und Verlässlichkeit (KASTEL), Karlsruher Institut für Technologie (KIT)
2,3; Weigl, Alexander
2,31 FZI Forschungszentrum Informatik (FZI)
2 Karlsruher Institut für Technologie (KIT)
3 Institut für Informationssicherheit und Verlässlichkeit (KASTEL), Karlsruher Institut für Technologie (KIT)
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 \IHM 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.
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 \IHM 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.
| Zugehörige Institution(en) am KIT | Institut für Informationssicherheit und Verlässlichkeit (KASTEL) |
| Publikationstyp | Forschungsbericht/Preprint |
| Publikationsdatum | 04.05.2022 |
| Sprache | Englisch |
| Identifikator | KITopen-ID: 1000145727 |
| Umfang | 20 S. |
| Bemerkung zur Veröffentlichung | Long Version |
| Schlagwörter | Real-world case study \and, Deductive Program Verification, Java Modeling Language, Verified Hash Map, Verified Data Structure, Cooperative Verification |