Abstract specifications for concurrent maps

DOI10.1007/978-3-662-54434-1_36MaRDI QIDQ2988678zbMATH OpenOpenAlexFDO

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

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

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

• Modular reasoning about separation of concurrent data structures
• An integrated specification and verification technique for highly concurrent data structures
• Steps in modular specifications for concurrent modules (invited tutorial paper)
• A perspective on specifying and verifying concurrent modules
• Expressive modular fine-grained concurrency specification

Cites work

• A Marriage of Rely/Guarantee and Separation Logic
• Abstract specifications for concurrent maps
• Caper
• Communicating state transition systems for fine-grained concurrent resources
• Deny-Guarantee Reasoning
• Expressive modular fine-grained concurrency specification
• scientific article; zbMATH DE number 2006660 (Why is no real title available?)
• Impredicative concurrent abstract predicates
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• Modular termination verification for non-blocking concurrency
• Permission accounting in separation logic
• Resources, concurrency, and local reasoning
• Specifying and verifying concurrent algorithms with histories and subjectivity
• Steps in modular specifications for concurrent modules (invited tutorial paper)
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
• Verifying linearizability with hindsight
• Views, compositional reasoning for concurrent programs

Cited in

(5)

• Resource protection using atomics. Patterns and verification
• Abstract specifications for concurrent maps
• Modular reasoning about separation of concurrent data structures
• Modular reasoning for deterministic parallelism
• Expressive modular fine-grained concurrency specification

Describes a project that uses

Uses Software

• Caper
• ConcurrentSkipListMap

This page was built for publication: Abstract specifications for concurrent maps

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