An ACL2 mechanization of an axiomatic framework for weak memory

DOI10.4204/EPTCS.152.11MaRDI QIDQ6589552zbMATH OpenFDO

Authors Benjamin Selfridge

Publication date 19 August 2024

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)

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

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)