Reuben N. S. Rowe, James Brotherston: Automatic cyclic termination proofs for recursive procedures in separation logic. CPP 2017: 53-65