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

DOI10.1145/3594729MaRDI QIDQ6611956zbMATH OpenFDO

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

Publication date 27 September 2024

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3594729

zbMATH Keywords

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

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Formal specification and verification of JDK's identity hash map implementation
• Proving JDK's dual pivot quicksort correct
• Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking
• Java bytecode verification: Algorithms and formalizations
• scientific article; zbMATH DE number 1706337

Cites work

• Behavioral interface specification languages
• Formal specification and verification of JDK's identity hash map implementation
• JMLUnit: the next generation
• Proving JDK's dual pivot quicksort correct
• Understanding parameters of deductive verification: an empirical investigation of KeY

Cited in

(2)

• First order Büchi automata and their application to verification of LTL specifications
• Verifying a realistic mutable hash table. Case study (short paper)

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 Q6611956)