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