BI as an assertion language for mutable data structures
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- A perspective on specifying and verifying concurrent modules
- Formally verifying exceptions for low-level code with separation logic
- Compositional entailment checking for a fragment of separation logic
- Unifying separation logic and region logic to allow interoperability
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- Program logic and equivalence in the presence of garbage collection.
- Model checking mobile ambients
- Bunched logics displayed
- Verify heaps via unified model checking
- Unifying decidable entailments in separation logic with inductive definitions
- An adaptation-complete proof system for local reasoning about cloud storage systems
- A stone-type duality theorem for separation logic via its underlying bunched logics
- Separation logic and logics with team semantics
- Strong-separation logic
- Automated repair of heap-manipulating programs using deductive synthesis
- Compositional satisfiability solving in separation logic
- Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules
- On the relation between concurrent separation logic and concurrent Kleene algebra
- Automated theorem proving by resolution in non-classical logics
- Coalgebraic completeness-via-canonicity for distributive substructural logics
- Separation logic with one quantified variable
- Completeness and expressiveness of pointer program verification by separation logic
- A logic of reachable patterns in linked data-structures
- Bunched sequential information
- Completeness for recursive procedures in separation logic
- Invariants synthesis over a combined domain for automated program verification
- Local reasoning about data update
- Systems modelling via resources and processes: philosophy, calculus, semantics, and logic
- A logic of separating modalities
- An epistemic separation logic
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- The essence of higher-order concurrent separation logic
- A higher-order logic for concurrent termination-preserving refinement
- The relationship between separation logic and implicit dynamic frames
- Tractable Reasoning in a Fragment of Separation Logic
- A machine-checked framework for relational separation logic
- Stone-type dualities for separation logics
- A unified display proof theory for bunched logic
- An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics
- Types, Maps and Separation Logic
- Undecidability of propositional separation logic and its neighbours
- Enhancing symbolic execution of heap-based programs with separation logic for test input generation
- Adjunct Elimination in Context Logic for Trees
- Formal verification of concurrent programs with Read-write locks
- On the Almighty Wand
- A Spatial Equational Logic for the Applied π-Calculus
- Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
- On the almighty wand
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- scientific article; zbMATH DE number 6970800 (Why is no real title available?)
- Separation logics and modalities: a survey
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- scientific article; zbMATH DE number 1841809 (Why is no real title available?)
- Interprocedural shape analysis for effectively cutpoint-free programs
- Bringing Order to the Separation Logic Jungle
- On temporal and separation logics
- scientific article; zbMATH DE number 7566073 (Why is no real title available?)
- scientific article; zbMATH DE number 7407781 (Why is no real title available?)
- A complete axiomatisation for quantifier-free separation logic
- Certified reasoning with infinity
- A substructural epistemic resource logic
- Convolution as a Unifying Concept
- Abstract hidden Markov models: a monadic account of quantitative information flow
- A public announcement separation logic
- Separation Logic for Multiple Inheritance
- Multimodal Separation Logic for Reasoning About Operational Semantics
- Reasoning about B+ trees with operational semantics and separation logic
- A type system with usage aspects
- An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
- Footprints in Local Reasoning
- Algebraic separation logic
- Separation Logic Contracts for a Java-Like Language with Fork/Join
- A Theory of Pointers for the UTP
- Two decades of automatic amortized resource analysis
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Program Verification with Separation Logic
- On Composing Finite Forests with Modal Logics
- An efficient cyclic entailment procedure in a fragment of separation logic
- An epistemic separation logic with action models
- A separation logic with histories of epistemic actions as resources
- An undecidability result for separation logic with theory reasoning
- Foundations for entailment checking in quantitative separation logic
- A fine-grained semantics for arrays and pointers under weak memory models
- An algebraic glimpse at bunched implications and separation logic
- Reasoning about sequences of memory states
- Structural operational semantics through context-dependent behaviour
- Concolic testing heap-manipulating programs
- Testing the satisfiability of formulas in separation logic with permissions
- Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
- Formally understanding Rust's ownership and borrowing system at the memory level
- Inferentialist resource semantics
- Decidable entailments in separation logic with inductive definitions: beyond establishment
- Deciding satisfiability for overlaid symbolic heaps
- The satisfiability problem in a separation logic of relations
- Idempotent resources in separation logic. The heart of \texttt{core} in Iris
- Tractable and intractable entailment problems in separation logic with inductively defined predicates
- Expressive completeness of separation logic in block-based cloud storage systems
- Expressiveness results for an inductive logic of separated relations
- A direct procedure to test entailment in a separation logic of relations
- A logical approach to type soundness
This page was built for publication: BI as an assertion language for mutable data structures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5178870)
