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 (58)
- Permission-based separation logic for multithreaded Java programs
- 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)
- Logical reasoning for disjoint permissions
- RustHorn: CHC-based verification for Rust programs
- Title not available (Why is that?)
- Precision and the conjunction rule in concurrent separation logic
- Disproving inductive entailments in separation logic via base pair approximation
- Separation Logic Contracts for a Java-Like Language with Fork/Join
- Refinement to imperative HOL
- Separation logics and modalities: a survey
- Reasoning over permissions regions in concurrent separation logic
- On the relation between concurrent separation logic and concurrent Kleene algebra
- The essence of higher-order concurrent separation logic
- Abstract local reasoning for concurrent libraries: mind the gap
- A semantics for concurrent separation logic
- A revisionist history of concurrent separation logic
- Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
- The relationship between separation logic and implicit dynamic frames
- Syntactic control of interference and concurrent separation logic
- Concurrent separation logic and operational semantics
- Tackling real-life relaxed concurrency with FSL++
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Concise read-only specifications for better synthesis of programs with pointers
- Resources, concurrency, and local reasoning
- Weak updates and separation logic
- A type system for borrowing permissions
- On Symbolic Heaps Modulo Permission Theories
- A perspective on specifying and verifying concurrent modules
- Abstract specifications for concurrent maps
- Footprints in Local Reasoning
- Barriers in Concurrent Separation Logic
- Order out of chaos: proving linearizability using local views
- Undecidability of propositional separation logic and its neighbours
- ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
- Separation Logic Semantics for Communicating Processes
- Certifying low-level programs with hardware interrupts and preemptive threads
- Refinement to Imperative/HOL
- Inter-process buffers in separation logic with rely-guarantee
- Verified software toolchain (invited talk)
- Fine-grained concurrency with separation logic
- Temporary read-only permissions for separation logic
- Permission-based separation logic for message-passing concurrency
- A program construction and verification tool for separation logic
- A verifiable low-level concurrent programming model based on colored Petri nets
- Formal verification of concurrent programs with Read-write locks
- Automatic inference of access permissions
- A formal C memory model for separation logic
- Strong-separation logic
- Efficient Verified Implementation of Introsort and Pdqsort
- On assertion-based encapsulation for object invariants and simulations
- Caper
- Polymorphic Fractional Capabilities
- Types, Maps and Separation Logic
- A game semantics of concurrent separation logic
- Fairness, resources, and separation
- Unified reasoning about robustness properties of symbolic-heap 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)
