Permission accounting in separation logic
DOI10.1145/1040305.1040327zbMATH Open1369.68130OpenAlexW2061341742WikidataQ130884290 ScholiaQ130884290MaRDI QIDQ5276151FDOQ5276151
Authors: Richard Bornat, Cristiano Calcagno, Matthew J. Parkinson, Peter W. O'Hearn 
Publication date: 14 July 2017
Published in: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1040305.1040327
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)
Cited In (54)
- Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
- Testing the satisfiability of formulas in separation logic with permissions
- Steps in modular specifications for concurrent modules (invited tutorial paper)
- Concurrent Separation Logic and Operational Semantics
- Title not available (Why is that?)
- Title not available (Why is that?)
- ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
- Separation Logic Contracts for a Java-Like Language with Fork/Join
- Refinement to imperative HOL
- Separation logics and modalities: a survey
- On the relation between concurrent separation logic and concurrent Kleene algebra
- Abstract local reasoning for concurrent libraries: mind the gap
- A semantics for concurrent separation logic
- Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
- The relationship between separation logic and implicit dynamic frames
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
- Fairness, Resources, and Separation
- Resources, concurrency, and local reasoning
- Weak updates and separation logic
- On Symbolic Heaps Modulo Permission Theories
- A perspective on specifying and verifying concurrent modules
- Footprints in Local Reasoning
- The Essence of Higher-Order Concurrent Separation Logic
- Barriers in Concurrent Separation Logic
- Disproving Inductive Entailments in Separation Logic via Base Pair Approximation
- Separation Logic Semantics for Communicating Processes
- Certifying low-level programs with hardware interrupts and preemptive threads
- Tackling Real-Life Relaxed Concurrency with FSL++
- Refinement to Imperative/HOL
- Syntactic Control of Interference and Concurrent Separation Logic
- Inter-process buffers in separation logic with rely-guarantee
- Verified software toolchain (invited talk)
- RustHorn: CHC-Based Verification for Rust Programs
- Fine-grained concurrency with separation logic
- Permission-based separation logic for message-passing concurrency
- Abstract Specifications for Concurrent Maps
- A verifiable low-level concurrent programming model based on colored Petri nets
- Formal verification of concurrent programs with Read-write locks
- Undecidability of Propositional Separation Logic and Its Neighbours
- Automatic inference of access permissions
- A formal C memory model for separation logic
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- Strong-separation logic
- Precision and the Conjunction Rule in Concurrent Separation Logic
- Temporary Read-Only Permissions for Separation Logic
- Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
- Efficient Verified Implementation of Introsort and Pdqsort
- On assertion-based encapsulation for object invariants and simulations
- A Program Construction and Verification Tool for Separation Logic
- Caper
- Polymorphic Fractional Capabilities
- A Revisionist History of Concurrent Separation Logic
- Types, Maps and Separation Logic
- A game semantics of concurrent separation logic
This page was built for publication: Permission accounting in separation logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5276151)
