swMATH28542MaRDI QIDQ40256FDOQ40256
Author name not available (Why is that?)
Official website: http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/
Cited In (42)
- 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
- SeLoger
- 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
- Predator
- HIP
- SLAyer
- Smallfoot
- VATA
- MTBDD
- Juggrnaut
- FunArray
- THOR
- coreStar
- Cyclist
- InKa
- Antichains
- Infer
- Tractability of separation logic with inductive definitions: beyond lists
- GRASShopper
- QuodLibet
- MSO_Regex_Equivalence
- A decision procedure for separation logic in SMT
- Rely
- 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
