Abstract local reasoning for concurrent libraries: mind the gap

DOI10.1016/j.entcs.2014.10.009zbMath1337.68069OpenAlexW2074635178WikidataQ113317846 ScholiaQ113317846MaRDI QIDQ283756

Adam Wright, Azalea Raad, Philippa Gardner, Mark Wheelhouse

Publication date: 13 May 2016

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

zbMATH Keywords

reasoningtranslationrefinementseparationconcurrencyabstraction

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Abstract local reasoning for concurrent libraries: mind the gap ⋮ DOM: Specification and Client Reasoning

Cites Work

• Abstract local reasoning for concurrent libraries: mind the gap
• Blaming the client: on data refinement in the presence of pointers
• Resources, concurrency, and local reasoning
• Fictional Separation Logic
• Views
• Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
• Permission accounting in separation logic
• Context logic and tree update
• Impredicative Concurrent Abstract Predicates
• Local Reasoning for the POSIX File System
• Unnamed Item

This page was built for publication: Abstract local reasoning for concurrent libraries: mind the gap