Model checking a cache coherence protocol of a Java DSM implementation

DOI10.1016/J.JLAP.2006.08.007zbMATH Open1106.68013OpenAlexW2112832542MaRDI QIDQ864512FDOQ864512

Authors: Jun Pang, Rutger Hofman, Ronald Veldema, Wan Fokkink 

Publication date: 9 February 2007

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2006.08.007

Recommendations

• Checking cache-coherence protocols with TLA\(^+\)
• Run‐time optimizations for a Java DSM implementation
• scientific article; zbMATH DE number 1830911
• scientific article; zbMATH DE number 2087408
• scientific article; zbMATH DE number 1951189

zbMATH Keywords

model checkingformal specification\(\mu\)CRLcache coherence protocolsJava memory model

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Fairness and related properties in transition systems - a temporal logic to deal with fairness
• Specification of abstract data types
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Process Algebra
• Efficient on-the-fly model-checking for regular alternation-free \(\mu\)-calculus
• Title not available (Why is that?)
• Algebraic process verification.
• Formal stystems specification. The RPC-memory specification case study
• Verification of a sliding window protocol in \(\mu\) CRL and PVS
• Linearization in parallel pCRL
• Analysis of a distributed system for lifting trucks.
• Title not available (Why is that?)
• Distributed branching bisimulation reduction of state spaces
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (8)

• State space reduction of linear processes using control flow reconstruction
• Checking cache-coherence protocols with TLA\(^+\)
• Run‐time optimizations for a Java DSM implementation
• Title not available (Why is that?)
• Symbolic Reachability for Process Algebras with Recursive Data Types
• Distributed branching bisimulation reduction of state spaces
• On-the-fly solving for symbolic parity games
• A database approach to distributed state space generation

This page was built for publication: Model checking a cache coherence protocol of a Java DSM implementation

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