Can we efficiently check concurrent programs under relaxed memory models in Maude?

DOI10.1007/978-3-319-12904-4_2MaRDI QIDQ2945130zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Yehia Abd Alrahman, Marina Andric, Alessandro Beggiato, Alberto Lluch Lafuente

Publication date 9 September 2015

Published in Rewriting Logic and Its Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-12904-4_2

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42)

Recommendations

• Effective abstractions for verification under relaxed memory models
• Effective Program Verification for Relaxed Memory Models
• Effective Abstractions for Verification under Relaxed Memory Models
• Studying Operational Models of Relaxed Concurrency
• On the verification problem for weak memory models

Cited in

(8)

• Model checking parameterized by the semantics in Maude
• Star-topology decoupled state space search
• Effective Program Verification for Relaxed Memory Models
• How Efficient Can Memory Checking Be?
• Star-Topology Decoupling in SPIN
• Operational semantics of a weak memory model with channel synchronization
• Operational semantics of a weak memory model with channel synchronization
• Parallelized sequential composition and hardware weak memory models

This page was built for publication: Can we efficiently check concurrent programs under relaxed memory models in Maude?

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