Slide

swMATH28542MaRDI QIDQ40256FDOQ40256

Author name not available (Why is that?)

Described by source

• Deciding entailments in inductive separation logic with tree automata

Cited In (23)

• Nested antichains for WS1S
• Title not available (Why is that?)
• Disproving inductive entailments in separation logic via base pair approximation
• Separation logics and modalities: a survey
• Decision Procedure for Entailment of Symbolic Heaps with Arrays
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• On temporal and separation logics
• Expressive completeness of separation logic with two variables and no separating conjunction
• Program Verification with Separation Logic
• Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules
• Two-Variable Separation Logic and Its Inner Circle
• Tractability of separation logic with inductive definitions: beyond lists
• A decision procedure for separation logic in SMT
• Juggrnaut: using graph grammars for abstracting unbounded heap structures
• Logic programming approach to automata-based decision procedures
• The tree width of separation logic with recursive definitions
• Automated mutual induction proof in separation logic
• Separation logic with one quantified variable
• Compositional entailment checking for a fragment of separation logic
• A complete decision procedure for linearly compositional separation logic with data constraints
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
• Lazy automata techniques for WS1S
• Unified reasoning about robustness properties of symbolic-heap separation logic

This page was built for software: Slide