Steps in modular specifications for concurrent modules (invited tutorial paper)

DOI10.1016/j.entcs.2015.12.002zbMath1351.68188OpenAlexW2208101949WikidataQ113317742 ScholiaQ113317742MaRDI QIDQ5971389

Philippa Gardner, Thomas Dinsdale-Young, Pedro da Rocha Pinto

Publication date: 16 December 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2015.12.002

zbMATH Keywords

concurrencyspecificationprogram verification

Mathematics Subject Classification ID

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 (2)

Abstract Specifications for Concurrent Maps ⋮ Modular Termination Verification for Non-blocking Concurrency

Cites Work

• Unnamed Item
• Resources, concurrency, and local reasoning
• Iris
• Views
• Subjective auxiliary state for coarse-grained concurrency
• Abstraction for Concurrent Objects
• Deny-Guarantee Reasoning
• Verifying properties of parallel programs
• Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
• Local rely-guarantee reasoning
• Permission accounting in separation logic
• Modular Reasoning about Separation of Concurrent Data Structures
• Expressive modular fine-grained concurrency specification
• Impredicative Concurrent Abstract Predicates
• Communicating State Transition Systems for Fine-Grained Concurrent Resources
• An axiomatic basis for computer programming
• Linearizability with Ownership Transfer

This page was built for publication: Steps in modular specifications for concurrent modules (invited tutorial paper)