A fine-grained semantics for arrays and pointers under weak memory models

DOI10.1007/978-3-031-27481-7_18zbMATH Open1529.68177MaRDI QIDQ6174541FDOQ6174541

Authors: Robert Colvin 

Publication date: 17 August 2023

Published in: Formal Methods (Search for Journal in Brave)

Recommendations

• Program verification under weak memory consistency using separation logic
• A wide-spectrum language for verification of programs on weak memory models
• Verification of Concurrent Programs on Weak Memory Models
• On the verification problem for weak memory models
• A formal hierarchy of weak memory models

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems
• Process algebra for synchronous communication
• BI as an assertion language for mutable data structures
• A semantics for concurrent separation logic
• An axiomatic basis for computer programming
• Views, compositional reasoning for concurrent programs
• Concurrent Kleene Algebra
• On Hoare logic and Kleene algebra with tests
• Tentative steps toward a development method for interfering programs
• A formal hierarchy of weak memory models
• Owicki-Gries reasoning for weak memory models
• Verifying concurrent data structures by simulation
• Communicating state transition systems for fine-grained concurrent resources
• A separation logic for a promising semantics
• Ogre and Pythia: an invariance proof method for weak consistency models
• A promising semantics for relaxed-memory concurrency
• An Efficient Algorithm for Exploiting Multiple Arithmetic Units
• Designing a semantic model for a wide-spectrum language with concurrency
• An algebra of synchronous atomic steps
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Parallelized sequential composition and hardware weak memory models

Cited In (1)

• Mathematics of Program Construction

This page was built for publication: A fine-grained semantics for arrays and pointers under weak memory models

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