BI as an assertion language for mutable data structures
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- Strong-separation logic
- On the Almighty Wand
- A machine-checked framework for relational separation logic
- A logic of reachable patterns in linked data-structures
- An epistemic separation logic with action models
- Tractable and intractable entailment problems in separation logic with inductively defined predicates
- scientific article; zbMATH DE number 6970800 (Why is no real title available?)
- A type system with usage aspects
- Invariants synthesis over a combined domain for automated program verification
- Local reasoning about data update
- Concolic testing heap-manipulating programs
- Testing the satisfiability of formulas in separation logic with permissions
- An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics
- A separation logic with histories of epistemic actions as resources
- Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
- Types, Maps and Separation Logic
- Certified reasoning with infinity
- Verify heaps via unified model checking
- Compositional satisfiability solving in separation logic
- Expressive completeness of separation logic in block-based cloud storage systems
- Bunched sequential information
- Adjunct elimination in context logic for trees
- A public announcement separation logic
- scientific article; zbMATH DE number 7566073 (Why is no real title available?)
- Expressiveness results for an inductive logic of separated relations
- Foundations for entailment checking in quantitative separation logic
- Algebra and logic for access control
- Structural operational semantics through context-dependent behaviour
- Interprocedural shape analysis for effectively cutpoint-free programs
- A direct procedure to test entailment in a separation logic of relations
- Separation Logic Contracts for a Java-Like Language with Fork/Join
- Enhancing symbolic execution of heap-based programs with separation logic for test input generation
- On the almighty wand
- On the relation between concurrent separation logic and concurrent Kleene algebra
- Separation logics and modalities: a survey
- Quantitative separation logic and programs with lists
- The essence of higher-order concurrent separation logic
- Completeness for recursive procedures in separation logic
- Separation Logic for Multiple Inheritance
- A calculus and logic of resources and processes
- Reasoning about sequences of memory states
- A higher-order logic for concurrent termination-preserving refinement
- A logical approach to type soundness
- Frame rule for mutually recursive procedures manipulating pointers
- Stone-type dualities for separation logics
- Bringing Order to the Separation Logic Jungle
- A substructural epistemic resource logic
- Multimodal Separation Logic for Reasoning About Operational Semantics
- Formal verification of C systems code. Structured types, separation logic and theorem proving
- The relationship between separation logic and implicit dynamic frames
- Convolution as a Unifying Concept
- Unfolding state variables improves model checking performance
- A complete axiomatisation for quantifier-free separation logic
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- A logic of separating modalities
- scientific article; zbMATH DE number 1841809 (Why is no real title available?)
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Abstract hidden Markov models: a monadic account of quantitative information flow
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- 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
- Separation logic and logics with team semantics
- On temporal and separation logics
- Algebraic separation logic
- Extending separation logic with fixpoints and postponed substitution
- Beyond symbolic heaps: deciding separation logic with inductive definitions
- Automated repair of heap-manipulating programs using deductive synthesis
- Tree-verifiable graph grammars
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- Completeness and expressiveness of pointer program verification by separation logic
- A perspective on specifying and verifying concurrent modules
- A stone-type duality theorem for separation logic via its underlying bunched logics
- What is decidable in separation logic beyond progress, connectivity and establishment?
- Day algebras
- Footprints in Local Reasoning
- Undecidability of propositional separation logic and its neighbours
- Concurrent weighted logic
- Model checking mobile ambients
- Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
- Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules
- Inferentialist resource semantics
- Program Verification with Separation Logic
- Decidable entailments in separation logic with inductive definitions: beyond establishment
- Reasoning about B+ trees with operational semantics and separation logic
- Certifying low-level programs with hardware interrupts and preemptive threads
- An undecidability result for separation logic with theory reasoning
- scientific article; zbMATH DE number 7407781 (Why is no real title available?)
- Automated theorem proving by resolution in non-classical logics
- Deciding satisfiability for overlaid symbolic heaps
- Adjunct Elimination in Context Logic for Trees
- Fine-grained concurrency with separation logic
- A calculus and logic of bunched resources and processes
- Unifying decidable entailments in separation logic with inductive definitions
- Relational separation logic
- Unifying separation logic and region logic to allow interoperability
- An epistemic separation logic
- Program logic and equivalence in the presence of garbage collection.
- An algebraic glimpse at bunched implications and separation logic
- Systems modelling via resources and processes: philosophy, calculus, semantics, and logic
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)
