Effective Program Verification for Relaxed Memory Models

DOI10.1007/978-3-540-70545-1_12MaRDI QIDQ3512487zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

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

Cited in

(23)

• Context-bounded analysis of TSO systems
• Effective Abstractions for Verification under Relaxed Memory Models
• 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
• Can we efficiently check concurrent programs under relaxed memory models in Maude?
• A verification-based approach to memory fence insertion in PSO memory systems
• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• Fences in weak memory models
• Verification of STM on relaxed memory models
• The impact of memory models on software reliability in multiprocessors
• 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

Describes a project that uses

Uses Software

• Checkfence
• veriSoft

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)