An ACL2 mechanization of an axiomatic framework for weak memory

DOI10.4204/EPTCS.152.11MaRDI QIDQ6589552FDOQ6589552

Authors: Benjamin Selfridge 

Publication date: 19 August 2024

Recommendations

• A formal hierarchy of weak memory models
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Verification of Concurrent Programs on Weak Memory Models
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
• A framework for correctness criteria on weak memory models

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

This page was built for publication: An ACL2 mechanization of an axiomatic framework for weak memory

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