Separation Logic. - O’HEARN, PETER (Communications of the ACM, 2019)
The article examines the use of separation logic in reasoning about computer programs. It looks at how separation logic supports scalable reasoning through the frame rule, an inference rule that allows a proof to be localized to the resources that a program component accesses. Concurrent separation logic is also covered.