Abstract Specifications for Concurrent Maps

DOI10.1007/978-3-662-54434-1_36zbMath1485.68078OpenAlexW2583024954MaRDI QIDQ2988678

Philippa Gardner, Gian Ntzik, Pedro da Rocha Pinto, Shale Xiong

Publication date: 19 May 2017

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

Full work available at URL: http://hdl.handle.net/10044/1/43740

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

Abstract Specifications for Concurrent Maps

Uses Software

• Caper
• ConcurrentSkipListMap

Cites Work

• Unnamed Item
• Resources, concurrency, and local reasoning
• Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
• Modular Termination Verification for Non-blocking Concurrency
• Iris
• Views
• Caper
• Abstract Specifications for Concurrent Maps
• A Marriage of Rely/Guarantee and Separation Logic
• Deny-Guarantee Reasoning
• Verifying linearizability with hindsight
• Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
• Permission accounting in separation logic
• Expressive modular fine-grained concurrency specification
• Impredicative Concurrent Abstract Predicates
• Communicating State Transition Systems for Fine-Grained Concurrent Resources
• Steps in modular specifications for concurrent modules (invited tutorial paper)