01
Separation Logic: Local Reasoning for Programs with Mutable Memory
Separation logic extended Hoare-style program reasoning with spatial connectives that let proofs describe disjoint pieces of memory, enabling local reasoning about pointers and later scalable automated analysis.
↗