Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models

DOI10.1007/978-3-642-19835-9_3zbMath1315.68084OpenAlexW1594825470MaRDI QIDQ3000633

Koushik Sen, Christos Stergiou, Jabob Burnim

Publication date: 19 May 2011

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-19835-9_3

Mathematics Subject Classification ID

Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (7)

Combining Model Checking and Testing ⋮ Verification of Concurrent Programs on Weak Memory Models ⋮ Stateless model checking for TSO and PSO ⋮ Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models ⋮ Deciding Robustness against Total Store Ordering ⋮ Context-Bounded Analysis of TSO Systems ⋮ CCA-Secure Keyed-Fully Homomorphic Encryption

Uses Software

• Checkfence

Cites Work

• Memory model sensitive bytecode verification
• Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models
• Effective Program Verification for Relaxed Memory Models
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• On the verification problem for weak memory models
• Dynamic partial-order reduction for model checking software
• Computer Aided Verification

This page was built for publication: Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models