SeparationLogic

Reasoning about a program that follows pointers is awkward for ordinary logic, because a statement about one part of memory can be invalidated by a change to another part that happens to be reachable from it.

Separation logic answers this by making the splitting of memory part of the language: a statement can assert that memory divides into two disjoint pieces, each satisfying its own description. What holds of one piece then keeps holding while the other is modified, so a program’s effect can be described in terms of the memory it actually touches.