Radu Iosif
6 references under this name, matched as it is written. Somebody else may write under it too, and the same person may appear here spelled another way.
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
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.
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