Java Memory Model-Aware Model Checking

DOI10.1007/978-3-642-28756-5_16MaRDI QIDQ2894274zbMATH OpenOpenAlexFDO

Authors Huafeng Jin, Tuba Yavuz-Kahveci, Beverly A. Sanders

Publication date 29 June 2012

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-28756-5_16

zbMATH Keywords

benign data racesmodel checkingrelaxed memory model

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Java and the Java memory model -- a unified, machine-checked formalisation
• The safety-critical Java memory model formalised
• scientific article; zbMATH DE number 1951189
• scientific article; zbMATH DE number 1617288
• The Java memory model
• scientific article; zbMATH DE number 1670563
• scientific article; zbMATH DE number 2087636

Cited in

(16)

• A local approach for temporal model checking of Java bytecode
• Model checking JAVA programs using JAVA PathFinder
• The safety-critical Java memory model formalised
• Memory model sensitive bytecode verification
• scientific article; zbMATH DE number 1617288 (Why is no real title available?)
• scientific article; zbMATH DE number 1670563 (Why is no real title available?)
• Java and the Java memory model -- a unified, machine-checked formalisation
• Formalising Java’s Data Race Free Guarantee
• scientific article; zbMATH DE number 1951189 (Why is no real title available?)
• scientific article; zbMATH DE number 2087636 (Why is no real title available?)
• The Java memory model
• Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making
• The Java Memory Model: Operationally, Denotationally, Axiomatically
• Local Data Race Freedom with Non-multi-copy Atomicity
• Model checking race-freedom when ``sequential consistency for data-race-free programs is guaranteed
• Automatic analysis of DMA races using model checking and k-induction

This page was built for publication: Java Memory Model-Aware Model Checking

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