Pages that link to "Item:Q5178870"
From MaRDI portal
The following pages link to BI as an assertion language for mutable data structures (Q5178870):
Displaying 42 items.
- A Higher-Order Logic for Concurrent Termination-Preserving Refinement (Q2988673) (← links)
- The Relationship between Separation Logic and Implicit Dynamic Frames (Q3000593) (← links)
- Tractable Reasoning in a Fragment of Separation Logic (Q3090833) (← links)
- A Machine-Checked Framework for Relational Separation Logic (Q3095237) (← links)
- (Q3121529) (← links)
- A Unified Display Proof Theory for Bunched Logic (Q3178253) (← links)
- An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics (Q3178265) (← links)
- Types, Maps and Separation Logic (Q3183535) (← links)
- Undecidability of Propositional Separation Logic and Its Neighbours (Q3189649) (← links)
- Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation (Q3297594) (← links)
- Adjunct Elimination in Context Logic for Trees (Q3498442) (← links)
- On the Almighty Wand (Q3540188) (← links)
- A Spatial Equational Logic for the Applied π-Calculus (Q3541032) (← links)
- Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding (Q3636908) (← links)
- (Q4553286) (← 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)
- Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs (Q4916088) (← links)
- Bringing Order to the Separation Logic Jungle (Q5055998) (← links)
- On Temporal and Separation Logics (Q5079764) (← links)
- (Q5094147) (← links)
- (Q5155670) (← links)
- (Q5155678) (← links)
- Certified Reasoning with Infinity (Q5206958) (← links)
- A Substructural Epistemic Resource Logic (Q5224495) (← links)
- Convolution as a Unifying Concept (Q5277916) (← links)
- (Q5376651) (← links)
- A public announcement separation logic (Q5377700) (← links)
- Separation Logic for Multiple Inheritance (Q5415606) (← links)
- Multimodal Separation Logic for Reasoning About Operational Semantics (Q5415628) (← links)
- Reasoning about B+ Trees with Operational Semantics and Separation Logic (Q5415648) (← links)
- A type system with usage aspects (Q5451967) (← links)
- An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures (Q5452601) (← links)
- Footprints in Local Reasoning (Q5458360) (← links)
- Separation Logic Contracts for a Java-Like Language with Fork/Join (Q5505424) (← links)
- A Theory of Pointers for the UTP (Q5505599) (← links)
- Two decades of automatic amortized resource analysis (Q5875892) (← links)
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions (Q5875940) (← links)
- Program Verification with Separation Logic (Q5883571) (← links)
- On Composing Finite Forests with Modal Logics (Q5886519) (← links)
- An epistemic separation logic with action models (Q6117141) (← links)
- An undecidability result for separation logic with theory reasoning (Q6161426) (← links)