Slide

swMATH28542MaRDI QIDQ40256

No author found.

Described by source

• Deciding Entailments in Inductive Separation Logic with Tree Automata

Related Items (23)

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction ⋮ Program Verification with Separation Logic ⋮ Decision Procedure for Entailment of Symbolic Heaps with Arrays ⋮ Disproving Inductive Entailments in Separation Logic via Base Pair Approximation ⋮ Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic ⋮ Logic programming approach to automata-based decision procedures ⋮ Separation logic with one quantified variable ⋮ Automated mutual induction proof in separation logic ⋮ Separation logics and modalities: a survey ⋮ Unnamed Item ⋮ Compositional entailment checking for a fragment of separation logic ⋮ Two-Variable Separation Logic and Its Inner Circle ⋮ Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic ⋮ Nested antichains for WS1S ⋮ Lazy Automata Techniques for WS1S ⋮ Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules ⋮ A decision procedure for separation logic in SMT ⋮ The Tree Width of Separation Logic with Recursive Definitions ⋮ Unnamed Item ⋮ On Temporal and Separation Logics ⋮ Juggrnaut: using graph grammars for abstracting unbounded heap structures ⋮ A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions

This page was built for software: Slide