Formal specification and verification of JDK's identity hash map implementation

DOI10.1007/978-3-031-07727-2_4zbMath1502.68054OpenAlexW4285124781MaRDI QIDQ2165501

Jonas Klamroth, Alexander Weigl, Christian Jung, Mattias Ulbrich, Martin J. M. de Boer, Stijn De Gouw

Publication date: 19 August 2022

Full work available at URL: https://doi.org/10.1007/978-3-031-07727-2_4

zbMATH Keywords

deductive program verificationcooperative verificationJava modeling languagereal-world case studyverified data structureverified hash map

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)

Related Items (3)

Generalized test tables: a domain-specific specification language for automated production systems ⋮ Integrating ADTs in KeY and their application to history-based reasoning about collection ⋮ IdentityHashMap

Uses Software

• JMLUnit
• KeY
• OpenJML
• JBMC

Cites Work

• Proving JDK's dual pivot quicksort correct
• Behavioral interface specification languages
• JMLUnit: The Next Generation

This page was built for publication: Formal specification and verification of JDK's identity hash map implementation