Communicating state transition systems for fine-grained concurrent resources

DOI10.1007/978-3-642-54833-8_16MaRDI QIDQ5410705zbMATH OpenOpenAlexFDO

Authors Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germán Andrés Delbianco

Publication date 16 April 2014

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-54833-8_16

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) 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)

Recommendations

• Fine-grained concurrency with separation logic
• CONCUR 2004 - Concurrency Theory
• Variables as resource for shared-memory programs: semantics and soundness
• A semantics for concurrent separation logic
• A revisionist history of concurrent separation logic

Cited in

(20)

• A state-based approach to communicating processes
• Dealing with final state sensitivity for synchronous communication
• A perspective on specifying and verifying concurrent modules
• Improving thread-modular abstract interpretation
• Specifying and verifying concurrent algorithms with histories and subjectivity
• Caper
• A higher-order logic for concurrent termination-preserving refinement
• Abstract specifications for concurrent maps
• Verifying concurrent graph algorithms
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Aneris: a mechanised logic for modular reasoning about distributed systems
• \textbf{Actris 2.0}: asynchronous session-type based reasoning in separation logic
• Steps in modular specifications for concurrent modules (invited tutorial paper)
• Concise outlines for a complex logic: a proof outline checker for TaDA
• A fine-grained semantics for arrays and pointers under weak memory models
• Practical abstractions for automated verification of message passing concurrency
• Dependent type refinements for futures
• A compositional theory of linearizability
• Correctness and concurrent complexity of the black-white bakery algorithm
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Communicating state transition systems for fine-grained concurrent resources

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