This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Radu Iosif
A grouping.
What can be decided about separation logic rather than what can be proved with it: tree width for recursive definitions, a decision procedure in SMT, and three records working the Bernays-Schönfinkel-Ramsey fragment, which is the standard way of asking where the decidable boundary falls. The sixth is SL-COMP, the benchmark that makes the answers comparable -- so the corpus can show the difference between a theorem and a solver that finishes.
6 references
The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
Mnacho Echenim and others (2020) · ACM Transactions on Computational Logic (TOCL)
SL-COMP: Competition of Solvers for Separation Logic
Mihaela Sighireanu and others (2019) · International Conference on Tools and Algorithms for the Construction and Analysis of Systems · Springer
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic
Mnacho Echenim and others (2018) · arXiv
Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic
Andrew Reynolds and others (2017) · 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) · Springer
A Decision Procedure for Separation Logic in SMT
Andrew Reynolds and others (2016) · Automated Technology for Verification and Analysis · Springer
The Tree Width of Separation Logic with Recursive Definitions
Radu Iosif and others (2013) · Automated Deduction – CADE-24 · Springer