Views, compositional reasoning for concurrent programs

DOI10.1145/2429069.2429104MaRDI QIDQ2931804zbMATH OpenOpenAlexFDO

Authors Thomas Dinsdale-Young, Philippa Gardner, Matthew J. Parkinson, Hongseok Yang, Lars Birkedal

Publication date 27 November 2014

Published in Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2429069.2429104

zbMATH Keywords

axiomatic semanticscompositional reasoningconcurrency

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Constructing the views framework
• Abstract patterns of compositional reasoning.
• scientific article; zbMATH DE number 3956417
• ColoSL: concurrent local subjective logic
• Compositional reasoning for shared-variable concurrent programs

Cited in

(32)

• A perspective on specifying and verifying concurrent modules
• Compositional reasoning for shared-variable concurrent programs
• Decision problems in a logic for reasoning about reconfigurable distributed systems
• A game semantics of concurrent separation logic
• On the relation between concurrent separation logic and concurrent Kleene algebra
• ColoSL: concurrent local subjective logic
• Modular termination verification for non-blocking concurrency
• Constructing the views framework
• Abstract local reasoning for concurrent libraries: mind the gap
• Subjective auxiliary state for coarse-grained concurrency
• On rely-guarantee reasoning
• A program construction and verification tool for separation logic
• Temporary read-only permissions for separation logic
• Caper
• Tackling real-life relaxed concurrency with FSL++
• A higher-order logic for concurrent termination-preserving refinement
• Abstract specifications for concurrent maps
• Verifying concurrent graph algorithms
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Aneris: a mechanised logic for modular reasoning about distributed systems
• Connecting higher-order separation logic to a first-order outside world
• Bringing Order to the Separation Logic Jungle
• Convolution as a Unifying Concept
• Steps in modular specifications for concurrent modules (invited tutorial paper)
• Concise outlines for a complex logic: a proof outline checker for TaDA
• A fine-grained semantics for arrays and pointers under weak memory models
• Make flows small again: revisiting the flow framework
• Rely-guarantee reasoning for causally consistent shared memory
• Idempotent resources in separation logic. The heart of \texttt{core} in Iris
• A logical approach to type soundness
• ConcurrentHOL
• Balancing expressiveness in formal approaches to concurrency

This page was built for publication: Views, compositional reasoning for concurrent programs

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