{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:23:38Z","timestamp":1779074618419,"version":"3.51.4"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T00:00:00Z","timestamp":1694563200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2023,9,30]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>\n            In this article, we present the first case study of the\n            <jats:monospace>IdentityHashMap<\/jats:monospace>\n            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.\n          <\/jats:p>","DOI":"10.1145\/3594729","type":"journal-article","created":{"date-parts":[[2023,5,18]],"date-time":"2023-05-18T12:15:16Z","timestamp":1684412116000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Formal Specification and Verification of JDK\u2019s\u00a0Identity Hash Map Implementation"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4794-6333","authenticated-orcid":false,"given":"Martin","family":"De Boer","sequence":"first","affiliation":[{"name":"Open University, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2964-6844","authenticated-orcid":false,"given":"Stijn","family":"De Gouw","sequence":"additional","affiliation":[{"name":"Open University, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8013-9453","authenticated-orcid":false,"given":"Jonas","family":"Klamroth","sequence":"additional","affiliation":[{"name":"FZI Research Center for Information Technology, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-6281-5297","authenticated-orcid":false,"given":"Christian","family":"Jung","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute of Technology, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2350-1831","authenticated-orcid":false,"given":"Mattias","family":"Ulbrich","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute of Technology, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8446-4598","authenticated-orcid":false,"given":"Alexander","family":"Weigl","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute of Technology, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,9,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_4"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_4"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-72308-2_3"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.149.8"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_28"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_10"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-07727-2_4"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6415339"},{"key":"e_1_3_2_11_2","first-page":"96","volume-title":"Proceedings of the 2021 Formal Methods in Computer Aided Design (FMCAD\u201921)","author":"Durand Timothee","year":"2021","unstructured":"Timothee Durand, Katalin Fazekas, Georg Weissenbacher, and Jakob Zwirchmayr. 2021. Model checking AUTOSAR components with CBMC. In Proceedings of the 2021 Formal Methods in Computer Aided Design (FMCAD\u201921). IEEE, 96\u2013101."},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2187671.2187678"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63461-2_11"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.538605"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-08166-8_14"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.284.5"},{"key":"e_1_3_2_18_2","unstructured":"Donald E Knuth. 1963. Notes on \u201cOpen\u201d Addressing. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.56.4899."},{"key":"e_1_3_2_19_2","unstructured":"Gary T. Leavens Erik Poll Curtis Clifton Yoonsik Cheon Clyde Ruby David Cok Peter M\u00fcller Joseph Kiniry Patrice Chalin Daniel M. Zimmerman et\u00a0al. 2008. JML Reference Manual."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2018.8341980"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_26"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018624"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47846-3_5"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-009-0106-5"},{"key":"e_1_3_2_26_2","volume-title":"Algorithms, (4th ed.).","author":"Sedgewick Robert","year":"2011","unstructured":"Robert Sedgewick and Kevin Wayne. 2011. Algorithms, (4th ed.).Addison-Wesley."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18070-5_13"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3594729","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3594729","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:51Z","timestamp":1750178271000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3594729"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,13]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,9,30]]}},"alternative-id":["10.1145\/3594729"],"URL":"https:\/\/doi.org\/10.1145\/3594729","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,13]]},"assertion":[{"value":"2022-10-13","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-04-12","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-09-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}