Rely-guarantee reasoning for causally consistent shared memory

DOI10.1007/978-3-031-37706-8_11zbMATH Open1547.68123MaRDI QIDQ6535633FDOQ6535633

Ori Lahav, Brijesh Dongol, Heike Wehrheim

Publication date: 1 February 2024

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Myths about the mutual exclusion problem
• Causal memory: definitions, implementation, and programming
• Views
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• An axiomatic proof technique for parallel programs
• Tentative steps toward a development method for interfering programs
• A calculus of durations
• A Marriage of Rely/Guarantee and Separation Logic
• The Rely-Guarantee method for verifying shared variable concurrent programs
• Verification of sequential and concurrent programs
• Owicki-Gries Reasoning for Weak Memory Models
• A separation logic for a promising semantics
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Ogre and Pythia: an invariance proof method for weak consistency models
• A promising semantics for relaxed-memory concurrency
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
• A complete axiom system for propositional interval temporal logic with infinite time
• On verifying causal consistency
• Reasoning about vectors using an SMT theory of sequences
• Taming release-acquire consistency
• The Benefits of Duality in Verifying Concurrent Programs under TSO
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Compositional reasoning for non-multicopy atomic architectures

This page was built for publication: Rely-guarantee reasoning for causally consistent shared memory

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