SLIDE - Separation Logic with Inductive Definitions. Automata-based entailment checking for Separation Logic with Inductive Definitions. SLIDE is a prototype tool for checking entailment in Separation Logic with user-provided inductive definitions of recursive data structures (lists, trees, and beyond). Basic features: Sound and complete for local data structures (doubly-linked lists, trees with parent pointers, etc.); Sound for non-local data structures (trees with linked leaves, skip-lists, etc. ); Built on top of the VATA tree automata library.

References in zbMATH (referenced in 20 articles , 1 standard article )

Showing results 1 to 20 of 20.
Sorted by year (citations)

  1. Echenim, Mnacho; Iosif, Radu; Peltier, Nicolas: Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules (2022)
  2. Kimura, Daisuke; Tatsuta, Makoto: Decidability for entailments of symbolic heaps with arrays (2021)
  3. Fiedor, Tomáš; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš: Nested antichains for WS1S (2019)
  4. Ta, Quang-Trung; Le, Ton Chanh; Khoo, Siau-Cheng; Chin, Wei-Ngan: Automated mutual induction proof in separation logic (2019)
  5. Chen, Taolue; Song, Fu; Wu, Zhilin: Tractability of separation logic with inductive definitions: beyond lists (2017)
  6. Demri, Stéphane; Galmiche, Didier; Larchey-Wendling, Dominique; Méry, Daniel: Separation logic with one quantified variable (2017)
  7. Enea, Constantin; Lengál, Ondřej; Sighireanu, Mihaela; Vojnar, Tomáš: Compositional entailment checking for a fragment of separation logic (2017)
  8. Fiedor, Tomáš; Holík, Lukáš; Janků, Petr; Lengál, Ondřej; Vojnar, Tomáš: Lazy automata techniques for WS1S (2017)
  9. Jansen, Christina; Katelaan, Jens; Matheja, Christoph; Noll, Thomas; Zuleger, Florian: Unified reasoning about robustness properties of symbolic-heap separation logic (2017)
  10. Unel, Gulay; Toman, David: Logic programming approach to automata-based decision procedures (2017)
  11. Demri, Stephane; Deters, Morgan: Expressive completeness of separation logic with two variables and no separating conjunction (2016)
  12. Gu, Xincai; Chen, Taolue; Wu, Zhilin: A complete decision procedure for linearly compositional separation logic with data constraints (2016)
  13. Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim: A decision procedure for separation logic in SMT (2016)
  14. Tatsuta, Makoto; Le, Quang Loc; Chin, Wei-Ngan: Decision procedure for separation logic with inductive definitions and Presburger arithmetic (2016)
  15. Brotherston, James; Gorogiannis, Nikos: Disproving inductive entailments in separation logic via base pair approximation (2015)
  16. Demri, Stéphane; Deters, Morgan: Separation logics and modalities: a survey (2015)
  17. Demri, Stéphane; Deters, Morgan: Two-variable separation logic and its inner circle (2015)
  18. Heinen, Jonathan; Jansen, Christina; Katoen, Joost-Pieter; Noll, Thomas: Juggrnaut: using graph grammars for abstracting unbounded heap structures (2015)
  19. Iosif, Radu; Rogalewicz, Adam; Vojnar, Tomáš: Deciding entailments in inductive separation logic with tree automata (2014)
  20. Iosif, Radu; Rogalewicz, Adam; Simacek, Jiri: The tree width of separation logic with recursive definitions (2013)