A perspective on specifying and verifying concurrent modules
DOI10.1016/j.jlamp.2018.03.003zbMath1395.68187OpenAlexW2796428443MaRDI QIDQ1648035
Philippa Gardner, Pedro da Rocha Pinto, Thomas Dinsdale-Young
Publication date: 27 June 2018
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlamp.2018.03.003
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)
Uses Software
Cites Work
- Unnamed Item
- A semantics for concurrent separation logic
- Resources, concurrency, and local reasoning
- Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
- CoLoSL: Concurrent Local Subjective Logic
- Modular Termination Verification for Non-blocking Concurrency
- Iris
- Views
- Subjective auxiliary state for coarse-grained concurrency
- Caper
- Abstraction for Concurrent Objects
- Deny-Guarantee Reasoning
- Verifying properties of parallel programs
- The Logic of Bunched Implications
- BI as an assertion language for mutable data structures
- Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
- Local rely-guarantee reasoning
- Separation logic and abstraction
- 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: A perspective on specifying and verifying concurrent modules
