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)

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

Describes a project that uses

Uses Software

• Apron
• z3

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)