Effective abstractions for verification under relaxed memory models

DOI10.1016/j.cl.2016.02.003zbMath1379.68237OpenAlexW2325560378MaRDI QIDQ681346

Eran Yahav, Martin Vechev, Yuri Meshman, 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

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

Related Items (6)

Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Unnamed Item ⋮ Robustness Against Transactional Causal Consistency. ⋮ Checking robustness between weak transactional consistency models ⋮ Unnamed Item

Uses Software

• Apron
• z3

Cites Work

• The octagon abstract domain
• 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
• Effective Program Verification for Relaxed Memory Models
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Software Verification for Weak Memory via Program Transformation
• CompCertTSO

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