Sound and complete monitoring of sequential consistency for relaxed memory models

DOI10.1007/978-3-642-19835-9_3MaRDI QIDQ3000633zbMATH OpenOpenAlexFDO

Authors Jabob Burnim, Koushik Sen, Christos Stergiou

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)

Recommendations

• Effective Program Verification for Relaxed Memory Models
• Stateless model checking for TSO and PSO
• Stateless model checking for TSO and PSO
• Effective abstractions for verification under relaxed memory models
• Effective Abstractions for Verification under Relaxed Memory Models

Cites work

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

Cited in

Describes a project that uses

Uses Software

• Checkfence

This page was built for publication: Sound and complete monitoring of sequential consistency for relaxed memory models

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