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 50 items.
- Bunched sequential information (Q266883) (← links)
- Completeness for recursive procedures in separation logic (Q278747) (← links)
- A logic of separating modalities (Q290917) (← links)
- Formal verification of concurrent programs with Read-write locks (Q351980) (← links)
- On the almighty wand (Q418137) (← links)
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400) (← links)
- Algebraic separation logic (Q549676) (← links)
- Reasoning about sequences of memory states (Q636268) (← links)
- Structural operational semantics through context-dependent behaviour (Q638568) (← links)
- Quantitative separation logic and programs with lists (Q707740) (← links)
- Frame rule for mutually recursive procedures manipulating pointers (Q732009) (← links)
- Fine-grained concurrency with separation logic (Q763473) (← links)
- Extending separation logic with fixpoints and postponed substitution (Q820139) (← links)
- Certifying low-level programs with hardware interrupts and preemptive threads (Q835764) (← links)
- Formal verification of C systems code. Structured types, separation logic and theorem proving (Q835768) (← links)
- A calculus and logic of resources and processes (Q855007) (← links)
- Relational separation logic (Q879369) (← links)
- Concurrent weighted logic (Q890620) (← links)
- A calculus and logic of bunched resources and processes (Q906271) (← links)
- Adjunct elimination in context logic for trees (Q964499) (← links)
- Algebra and logic for access control (Q968301) (← links)
- A perspective on specifying and verifying concurrent modules (Q1648035) (← links)
- Formally verifying exceptions for low-level code with separation logic (Q1683698) (← links)
- Compositional entailment checking for a fragment of separation logic (Q1688543) (← links)
- Unifying separation logic and region logic to allow interoperability (Q1798668) (← links)
- Possible worlds and resources: The semantics of \(\mathbf{BI}\) (Q1826634) (← links)
- Program logic and equivalence in the presence of garbage collection. (Q1874283) (← links)
- Model checking mobile ambients (Q1884885) (← links)
- Bunched logics displayed (Q1935559) (← links)
- Verify heaps via unified model checking (Q1986561) (← links)
- Unifying decidable entailments in separation logic with inductive definitions (Q2055854) (← links)
- An adaptation-complete proof system for local reasoning about cloud storage systems (Q2072067) (← links)
- A stone-type duality theorem for separation logic via its underlying bunched logics (Q2130585) (← links)
- Separation logic and logics with team semantics (Q2172820) (← links)
- Strong-separation logic (Q2233486) (← links)
- Automated repair of heap-manipulating programs using deductive synthesis (Q2234087) (← links)
- Compositional satisfiability solving in separation logic (Q2234106) (← links)
- Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules (Q2234797) (← links)
- On the relation between concurrent separation logic and concurrent Kleene algebra (Q2347904) (← links)
- Automated theorem proving by resolution in non-classical logics (Q2385426) (← links)
- Coalgebraic completeness-via-canonicity for distributive substructural logics (Q2409626) (← links)
- Separation logic with one quantified variable (Q2411038) (← links)
- Completeness and expressiveness of pointer program verification by separation logic (Q2417849) (← links)
- A logic of reachable patterns in linked data-structures (Q2643337) (← links)
- Invariants Synthesis over a Combined Domain for Automated Program Verification (Q2842643) (← links)
- Local Reasoning about Data Update (Q2864149) (← links)
- Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic (Q2864163) (← links)
- An Epistemic Separation Logic (Q2947467) (← links)
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic (Q2961583) (← links)
- The Essence of Higher-Order Concurrent Separation Logic (Q2988664) (← links)