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

Showing results 1 to 18 of 18.
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. Fiedor, Tomáš; Holík, Lukáš; Janků, Petr; Lengál, Ondřej; Vojnar, Tomáš: Lazy automata techniques for WS1S (2017)
  7. Jansen, Christina; Katelaan, Jens; Matheja, Christoph; Noll, Thomas; Zuleger, Florian: Unified reasoning about robustness properties of symbolic-heap separation logic (2017)
  8. Unel, Gulay; Toman, David: Logic programming approach to automata-based decision procedures (2017)
  9. Demri, Stephane; Deters, Morgan: Expressive completeness of separation logic with two variables and no separating conjunction (2016)
  10. Gu, Xincai; Chen, Taolue; Wu, Zhilin: A complete decision procedure for linearly compositional separation logic with data constraints (2016)
  11. Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim: A decision procedure for separation logic in SMT (2016)
  12. Tatsuta, Makoto; Le, Quang Loc; Chin, Wei-Ngan: Decision procedure for separation logic with inductive definitions and Presburger arithmetic (2016)
  13. Brotherston, James; Gorogiannis, Nikos: Disproving inductive entailments in separation logic via base pair approximation (2015)
  14. Demri, Stéphane; Deters, Morgan: Two-variable separation logic and its inner circle (2015)
  15. Demri, Stéphane; Deters, Morgan: Separation logics and modalities: a survey (2015)
  16. Heinen, Jonathan; Jansen, Christina; Katoen, Joost-Pieter; Noll, Thomas: Juggrnaut: using graph grammars for abstracting unbounded heap structures (2015)
  17. Iosif, Radu; Rogalewicz, Adam; Vojnar, Tomáš: Deciding entailments in inductive separation logic with tree automata (2014)
  18. Iosif, Radu; Rogalewicz, Adam; Simacek, Jiri: The tree width of separation logic with recursive definitions (2013)