Subjective auxiliary state for coarse-grained concurrency

DOI10.1145/2429069.2429134zbMath1301.68102OpenAlexW2137554739MaRDI QIDQ2931839

Aleksandar Nanevski, Ruy Ley-Wild

Publication date: 27 November 2014

Published in: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2429069.2429134

zbMATH Keywords

verificationconcurrencydependent type theorylocal reasoningrely-guarantee thinking

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (8)

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems ⋮ Connecting Higher-Order Separation Logic to a First-Order Outside World ⋮ A perspective on specifying and verifying concurrent modules ⋮ Steps in modular specifications for concurrent modules (invited tutorial paper) ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ Tackling Real-Life Relaxed Concurrency with FSL++ ⋮ Unnamed Item ⋮ On the relation between concurrent separation logic and concurrent Kleene algebra

Uses Software

• Coq

This page was built for publication: Subjective auxiliary state for coarse-grained concurrency