Permission accounting in separation logic
From MaRDI portal
Publication:5276151
DOI10.1145/1040305.1040327zbMath1369.68130OpenAlexW2061341742MaRDI QIDQ5276151
Cristiano Calcagno, Matthew J. Parkinson, Richard Bornat, 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
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Formal verification of parallel prefix sum and stream compaction algorithms in CUDA, Concise Read-Only Specifications for Better Synthesis of Programs with Pointers, RustHorn: CHC-Based Verification for Rust Programs, ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs, Abstract local reasoning for concurrent libraries: mind the gap, Automatic Inference of Access Permissions, A game semantics of concurrent separation logic, Certifying low-level programs with hardware interrupts and preemptive threads, Efficient Verified Implementation of Introsort and Pdqsort, Caper, Fairness, Resources, and Separation, Syntactic Control of Interference and Concurrent Separation Logic, Disproving Inductive Entailments in Separation Logic via Base Pair Approximation, Types, Maps and Separation Logic, A perspective on specifying and verifying concurrent modules, On assertion-based encapsulation for object invariants and simulations, Undecidability of Propositional Separation Logic and Its Neighbours, A verifiable low-level concurrent programming model based on colored Petri nets, Formal verification of concurrent programs with Read-write locks, A semantics for concurrent separation logic, Resources, concurrency, and local reasoning, A Program Construction and Verification Tool for Separation Logic, Refinement to Imperative/HOL, Inter-process buffers in separation logic with rely-guarantee, Separation logics and modalities: a survey, A formal C memory model for separation logic, Steps in modular specifications for concurrent modules (invited tutorial paper), Iris from the ground up: A modular foundation for higher-order concurrent separation logic, Temporary Read-Only Permissions for Separation Logic, Tackling Real-Life Relaxed Concurrency with FSL++, Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic, The Essence of Higher-Order Concurrent Separation Logic, Abstract Specifications for Concurrent Maps, Verified Software Toolchain, Barriers in Concurrent Separation Logic, The Relationship between Separation Logic and Implicit Dynamic Frames, Strong-separation logic, Refinement to imperative HOL, Footprints in Local Reasoning, Separation Logic Semantics for Communicating Processes, Weak updates and separation logic, A Revisionist History of Concurrent Separation Logic, Precision and the Conjunction Rule in Concurrent Separation Logic, Concurrent Separation Logic and Operational Semantics, Unnamed Item, Polymorphic Fractional Capabilities, Fine-grained concurrency with separation logic, Separation Logic Contracts for a Java-Like Language with Fork/Join, On the relation between concurrent separation logic and concurrent Kleene algebra, On Symbolic Heaps Modulo Permission Theories