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 17 articles , 1 standard article )

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

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