Pages that link to "Item:Q5276151"
From MaRDI portal
The following pages link to Permission accounting in separation logic (Q5276151):
Displaying 50 items.
- Abstract local reasoning for concurrent libraries: mind the gap (Q283756) (← links)
- A verifiable low-level concurrent programming model based on colored Petri nets (Q350966) (← links)
- Formal verification of concurrent programs with Read-write locks (Q351980) (← links)
- Inter-process buffers in separation logic with rely-guarantee (Q613139) (← links)
- Fine-grained concurrency with separation logic (Q763473) (← links)
- Certifying low-level programs with hardware interrupts and preemptive threads (Q835764) (← links)
- A semantics for concurrent separation logic (Q879367) (← links)
- Resources, concurrency, and local reasoning (Q879368) (← links)
- A perspective on specifying and verifying concurrent modules (Q1648035) (← links)
- A formal C memory model for separation logic (Q1694027) (← links)
- Refinement to imperative HOL (Q1739909) (← links)
- Weak updates and separation logic (Q1758657) (← links)
- Formal verification of parallel prefix sum and stream compaction algorithms in CUDA (Q2120963) (← links)
- A game semantics of concurrent separation logic (Q2130597) (← links)
- Strong-separation logic (Q2233486) (← links)
- On the relation between concurrent separation logic and concurrent Kleene algebra (Q2347904) (← links)
- On assertion-based encapsulation for object invariants and simulations (Q2643129) (← links)
- Automatic Inference of Access Permissions (Q2891412) (← links)
- A Program Construction and Verification Tool for Separation Logic (Q2941173) (← links)
- Refinement to Imperative/HOL (Q2945637) (← links)
- Temporary Read-Only Permissions for Separation Logic (Q2988642) (← links)
- Caper (Q2988651) (← links)
- Tackling Real-Life Relaxed Concurrency with FSL++ (Q2988652) (← links)
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic (Q2988661) (← links)
- The Essence of Higher-Order Concurrent Separation Logic (Q2988664) (← links)
- Abstract Specifications for Concurrent Maps (Q2988678) (← links)
- Verified Software Toolchain (Q3000569) (← links)
- Barriers in Concurrent Separation Logic (Q3000585) (← links)
- The Relationship between Separation Logic and Implicit Dynamic Frames (Q3000593) (← links)
- Fairness, Resources, and Separation (Q3178252) (← links)
- Syntactic Control of Interference and Concurrent Separation Logic (Q3178275) (← links)
- Types, Maps and Separation Logic (Q3183535) (← links)
- Undecidability of Propositional Separation Logic and Its Neighbours (Q3189649) (← links)
- Polymorphic Fractional Capabilities (Q3392918) (← links)
- Disproving Inductive Entailments in Separation Logic via Base Pair Approximation (Q3455777) (← links)
- Separation logics and modalities: a survey (Q4586138) (← links)
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic (Q4625160) (← links)
- Concise Read-Only Specifications for Better Synthesis of Programs with Pointers (Q5041091) (← links)
- RustHorn: CHC-Based Verification for Rust Programs (Q5041108) (← links)
- ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs (Q5041118) (← links)
- Efficient Verified Implementation of Introsort and Pdqsort (Q5049010) (← links)
- (Q5090915) (← links)
- On Symbolic Heaps Modulo Permission Theories (Q5136317) (← links)
- Separation Logic Semantics for Communicating Processes (Q5415605) (← links)
- Footprints in Local Reasoning (Q5458360) (← links)
- Separation Logic Contracts for a Java-Like Language with Fork/Join (Q5505424) (← links)
- A Revisionist History of Concurrent Separation Logic (Q5739348) (← links)
- Precision and the Conjunction Rule in Concurrent Separation Logic (Q5739357) (← links)
- Concurrent Separation Logic and Operational Semantics (Q5739365) (← links)
- Steps in modular specifications for concurrent modules (invited tutorial paper) (Q5971389) (← links)