Separation Logic of Generic Resources via Sheafeology

Berend van Starkenburg, Henning Basold, Chase Ford

Separation logic was conceived in order to make the verification of pointer programs scalable to large systems and it has proven extremely effective. The key idea is that programs…