Separation Logic: The Frame Rule, Separating Conjunction, and Concurrent VerificationAn exploration of separation logic—O'Hearn and Reynolds's revolutionary extension of Hoare logic for local reasoning about mutable state, the frame rule, and concurrent separation logic.
