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.
Makoto Tatsuta
A grouping.
One question asked four times over ten years, each time of a larger fragment: completeness for separation logic, from pointer program verification through inductive definitions and recursive procedures to expressiveness. The 2014 paper is the join between the corpus's two completeness lines, the Hoare-logic one and this one. A fifth record takes the decidability side, on a decidable fragment with inductive predicates and arithmetic.
4 references
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
Quang Loc Le and others (2017) · Computer Aided Verification · Springer
Completeness for recursive procedures in separation logic
Mahmudul Faisal Al Ameen and others (2016) · Theoretical Computer Science · Elsevier
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