We have a new paper on combining separation logic and refinement types to verify C code, appearing at POPL 2023 in a couple of months. It's called CN: Verifying Systems C Code with Separation-Logic Refinement Types, and it's by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and me.
