{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,9]],"date-time":"2026-09-09T02:13:42Z","timestamp":1788920022744,"version":"build-2803163510"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031634970","type":"print"},{"value":"9783031634987","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In this work, we verify, using the Stainless program verifier, the mutable  from the Scala standard library, a hash table using open addressing within a single array. As an executable specification, we write an immutable map based on a list of tuples and verify it against the mathematical definition of a map. We then show that \u2019s operations correspond to operations of this association list. To express the resizing of the hash table array, we introduce a new reference-swapping construct in Stainless. This allows us to apply the decorator design pattern without introducing aliasing. Our verification effort led us to find and fix a bug in the original implementation that manifests for large hash tables. Our performance analysis shows the verified version to be within a 1.5 factor of the original data structure.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_18","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"304-314","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Verifying a\u00a0Realistic Mutable Hash Table"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-9751-9252","authenticated-orcid":false,"given":"Samuel","family":"Chassot","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7044-9522","authenticated-orcid":false,"given":"Viktor","family":"Kun\u010dak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book, Lecture Notes in Computer Science, vol. 10001. Springer International Publishing, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6, http:\/\/link.springer.com\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"18_CR2","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: A versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 415\u2013442. Springer International Publishing, Cham (2022)"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-030-61362-4_4","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"B Beckert","year":"2020","unstructured":"Beckert, B., Kirsten, M., Klamroth, J., Ulbrich, M.: Modular verification of JML contracts using bounded model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 60\u201380. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_4"},{"key":"18_CR5","unstructured":"Bucev, M., Kun\u010dak, V.: Formally verified Quite OK Image format. In: Formal Methods in Computer-Aided Design (FMCAD) (2022)"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Chassot, S., Kun\u010dak, V.: Verifying a Realistic Mutable Hash Table Case Study (Short Paper) (Artifact) (Apr 2024). https:\/\/doi.org\/10.5281\/zenodo.11079220","DOI":"10.5281\/zenodo.11079220"},{"key":"18_CR7","unstructured":"Commit: New mutable hash map with long keys. https:\/\/github.com\/scala\/scala\/commit\/05aedd936e7e7bcf0fa2443abd58b39732f173a9"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"De\u00a0Boer, M., De\u00a0Gouw, S., Klamroth, J., Jung, C., Ulbrich, M., Weigl, A.: Formal specification and verification of JDK\u2019s identity hash map implementation. Formal Aspects Comput. 35(3), 18:1\u201318:26 (Sep 2023). https:\/\/doi.org\/10.1145\/3594729, https:\/\/dl.acm.org\/doi\/10.1145\/3594729","DOI":"10.1145\/3594729"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Guilloud, S., Bucev, M., Milovan\u010devi\u0107, D., Kun\u010dak, V.: Formula normalizations in verification. In: Computer-Aided Verification (CAV) (2023)","DOI":"10.1007\/978-3-031-37709-9_19"},{"issue":"6","key":"18_CR11","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1145\/359605.359618","volume":"20","author":"JV Guttag","year":"1977","unstructured":"Guttag, J.V.: Abstract data type and the development of data structures. Commun. ACM 20(6), 396\u2013404 (1977). https:\/\/doi.org\/10.1145\/359605.359618","journal-title":"Commun. ACM"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Hamza, J., Felix, S., Kun\u010dak, V., Nussbaumer, I., Schramka, F.: From verified Scala to STIX file system embedded code using Stainless. In: NASA Formal Methods (NFM), p.\u00a018 (2022). http:\/\/infoscience.epfl.ch\/record\/292424","DOI":"10.1007\/978-3-031-06773-0_21"},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Hamza, J., Voirol, N., Kun\u010dak, V.: System fr: formalized foundations for the stainless verifier. Proc. ACM Program. Lang. 3(OOPSLA) (oct 2019). https:\/\/doi.org\/10.1145\/3360592","DOI":"10.1145\/3360592"},{"key":"18_CR14","unstructured":"Hance, T., Lattuada, A., Hawblitzel, C., Howell, J., Johnson, R., Parno, B.: Storage Systems are Distributed Systems (So Verify Them That Way!). In: 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI) (2020)"},{"issue":"5","key":"18_CR15","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1109\/32.90445","volume":"17","author":"DE Harms","year":"1991","unstructured":"Harms, D.E., Weide, B.W.: Copying and swapping: influences on the design of reusable software components. IEEE Trans. Software Eng. 17(5), 424\u2013435 (1991). https:\/\/doi.org\/10.1109\/32.90445","journal-title":"IEEE Trans. Software Eng."},{"key":"18_CR16","doi-asserted-by":"publisher","unstructured":"Jackson, D., Damon, C.A.: Elements of style: analyzing a software design feature with a counterexample detector. ACM SIGSOFT Softw. Eng. Notes 21(3), 239\u2013249 (May 1996). https:\/\/doi.org\/10.1145\/226295.226322, https:\/\/dl.acm.org\/doi\/10.1145\/226295.226322","DOI":"10.1145\/226295.226322"},{"key":"18_CR17","unstructured":"Jahob Hashtables Codebase. https:\/\/github.com\/epfl-lara\/jahob\/tree\/master\/examples\/containers\/hashtable"},{"key":"18_CR18","unstructured":"Kuncak, V.: Modular Data Structure Verification. Ph.D. thesis, EECS Department, Massachusetts Institute of Technology (Feb 2007). http:\/\/hdl.handle.net\/1721.1\/38533"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Madhavan, R., Kulal, S., Kuncak, V.: Contract-based resource verification for higher-order functions with memoization. ACM SIGPLAN Notices 52(1), 330\u2013343 (Jan 2017). https:\/\/doi.org\/10.1145\/3093333.3009874, https:\/\/dl.acm.org\/doi\/10.1145\/3093333.3009874","DOI":"10.1145\/3093333.3009874"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Milovan\u010devi\u0107, D., Kun\u010dak, V.: Proving and disproving equivalence of functional programming assignments. In: ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI) (2023)","DOI":"10.1145\/3591258"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Generalized, efficient array decision procedures. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA, pp. 45\u201352. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351142","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"18_CR23","doi-asserted-by":"publisher","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. Formal Aspects Comput. 30(5), 495\u2013523 (Sep 2018). https:\/\/doi.org\/10.1007\/s00165-017-0435-1, https:\/\/doi.org\/10.1007\/s00165-017-0435-1","DOI":"10.1007\/s00165-017-0435-1"},{"key":"18_CR24","unstructured":"HashMap Scala Standard Library. https:\/\/scala-lang.org\/api\/3.3.1\/scala\/collection\/mutable\/HashMap.html"},{"key":"18_CR25","unstructured":"LongMap Specification. https:\/\/github.com\/scala\/scala\/blob\/263e5bd60d9c3947d8d17b7d8769a4b94f6865c7\/src\/library\/scala\/collection\/mutable\/LongMap.scala#L36"},{"key":"18_CR26","unstructured":"LongMap Implementation - Standard Library. https:\/\/github.com\/scala\/scala\/blob\/948ed0b60466803f404d5f24a3afc0a89c06ffc1\/src\/library\/scala\/collection\/mutable\/LongMap.scala"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Team, T.C.D.: The Coq Proof Assistant (Jun 2023). https:\/\/doi.org\/10.5281\/ZENODO.1003420. https:\/\/zenodo.org\/record\/1003420, language: en","DOI":"10.5281\/ZENODO.1003420"},{"key":"18_CR28","doi-asserted-by":"publisher","unstructured":"Voirol, N.C.Y.: Verified functional programming, p.\u00a0229 (2019). https:\/\/doi.org\/10.5075\/epfl-thesis-9479","DOI":"10.5075\/epfl-thesis-9479"},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: ACM SIGPLAN Conference Programming Language Design and Implementation (PLDI) (2008)","DOI":"10.1145\/1375581.1375624"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63498-7_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:39Z","timestamp":1747592259000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_18"}},"subtitle":["Case Study (Short Paper)"],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}