Effective Program Verification for Relaxed Memory Models
DOI10.1007/978-3-540-70545-1_12zbMATH Open1155.68428OpenAlexW2105980774MaRDI QIDQ3512487FDOQ3512487
Authors: Sebastian Burckhardt, Madanlal Musuvathi 
Publication date: 15 July 2008
Published in: Computer Aided Verification (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-70545-1_12
Recommendations
- Effective abstractions for verification under relaxed memory models
- Effective Abstractions for Verification under Relaxed Memory Models
- Sound and complete monitoring of sequential consistency for relaxed memory models
- Can we efficiently check concurrent programs under relaxed memory models in Maude?
- Program verification under weak memory consistency using separation logic
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (23)
- Abstract semantic diffing of evolving concurrent programs
- Model checking concurrent programs
- Formal memory models for the verification of low-level operating-system code
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Stateless model checking for TSO and PSO
- Deciding Robustness against Total Store Ordering
- A verification-based approach to memory fence insertion in PSO memory systems
- Can we efficiently check concurrent programs under relaxed memory models in Maude?
- An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
- The impact of memory models on software reliability in multiprocessors
- Fences in weak memory models
- Verification of STM on relaxed memory models
- Observation-based concurrent program logic for relaxed memory consistency models
- CCA-secure keyed-fully homomorphic encryption
- A load-buffer semantics for total store ordering
- Explaining relaxed memory models with program transformations
- Sound and complete monitoring of sequential consistency for relaxed memory models
- A formal hierarchy of weak memory models
- Automatic verification of RMA programs via abstraction extrapolation
- Verification of Concurrent Programs on Weak Memory Models
- Effective abstractions for verification under relaxed memory models
- Context-bounded analysis of TSO systems
- Effective Abstractions for Verification under Relaxed Memory Models
Uses Software
This page was built for publication: Effective Program Verification for Relaxed Memory Models
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3512487)
