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.
Wei-Ngan Chin
A grouping.
Completeness and decidability for pointer programs -- whether a separation-logic proof system can prove everything true of the programs it describes. Three records with Tatsuta run from completeness of pointer program verification through inductive definitions to expressiveness; two more take the decidability side, in a decidable fragment with inductive predicates and arithmetic, and the SL-COMP benchmark. This is the page where the relative-completeness question asked of Hoare logic is asked of the newer logic.
4 references
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
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
Quang Loc Le and others (2017) · Computer Aided Verification · Springer
Completeness of separation logic with inductive definitions for program verification
Makoto Tatsuta and others (2014) · International Conference on Software Engineering and Formal Methods · Springer
Completeness of Pointer Program Verification by Separation Logic
Makoto Tatsuta and others (2009) · 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods · IEEE