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

DOI10.1007/978-3-031-07727-2_4MaRDI QIDQ2165501zbMATH OpenOpenAlexFDO

Authors Jonas Klamroth, Christian Jung, Mattias Ulbrich, Alexander Weigl, 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

cooperative verificationdeductive program verificationJava modeling languagereal-world case studyverified data structureverified hash map

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1706337
• Java bytecode verification: Algorithms and formalizations
• Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking
• Improving the official specification of Java bytecode verification
• scientific article; zbMATH DE number 1796120
• scientific article; zbMATH DE number 5499373

Cites work

• Behavioral interface specification languages
• JMLUnit: the next generation
• Proving JDK's dual pivot quicksort correct

Cited in

(5)

• Proving JDK's dual pivot quicksort correct
• IdentityHashMap
• 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
• Formal specification and verification of JDK's identity hash map implementation

Describes a project that uses

Uses Software

• KeY
• JBMC
• JMLUnit
• OpenJML

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2165501)