Effective abstractions for verification under relaxed memory models

DOI10.1016/J.CL.2016.02.003MaRDI QIDQ681346zbMATH OpenOpenAlexFDO

Authors Yuri Meshman, Martin Vechev, Eran Yahav, Andrei Marian Dan

Publication date 30 January 2018

Published in Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.cl.2016.02.003

zbMATH Keywords

abstract interpretationrelaxed memory models

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 Program Verification for Relaxed Memory Models
• Relational thread-modular abstract interpretation under relaxed memory models
• On the verification problem for weak memory models
• Verification of STM on relaxed memory models

Cites work

• CompCertTSO
• Effective Program Verification for Relaxed Memory Models
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Programming languages and systems. 22nd European symposium on programming, ESOP 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16--24, 2013. Proceedings
• Software verification for weak memory via program transformation
• The octagon abstract domain

Cited in

(28)

• Effective Abstractions for Verification under Relaxed Memory Models
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
• LMS-Verify: abstraction without regret for verified systems programming
• Effective Program Verification for Relaxed Memory Models
• Static Analysis Via Abstract Interpretation of the Happens-Before Memory Model
• Software Transactional Memory on Relaxed Memory Models
• Formal memory models for the verification of low-level operating-system code
• Relational thread-modular abstract interpretation under relaxed memory models
• Checking robustness between weak transactional consistency models
• The decidability of verification under PS 2.0
• Tackling real-life relaxed concurrency with FSL++
• Can we efficiently check concurrent programs under relaxed memory models in Maude?
• A verification-based approach to memory fence insertion in PSO memory systems
• Software verification for weak memory via program transformation
• On the verification problem for weak memory models
• Verification of STM on relaxed memory models
• Thread-modular analysis of release-acquire concurrency
• A load-buffer semantics for total store ordering
• Stateless model checking for TSO and PSO
• Library abstraction for C/C++ concurrency
• Sound and complete monitoring of sequential consistency for relaxed memory models
• scientific article; zbMATH DE number 7327945 (Why is no real title available?)
• scientific article; zbMATH DE number 1857502 (Why is no real title available?)
• Computer Aided Verification
• Robustness Against Transactional Causal Consistency.
• The benefits of duality in verifying concurrent programs under TSO
• Automatic verification of RMA programs via abstraction extrapolation

Describes a project that uses

Uses Software

• z3
• Apron

This page was built for publication: Effective abstractions for verification under relaxed memory models

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