Quiver: Guided abductive inference of separation logic specifications in coq
S. Spies, L. Gäher, M.J. Sammler, D. Dreyer, Proceedings of the ACM on Programming Languages 8 (2024) 889–913.