Separation logic

In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Rod Burstall. The assertion language of separation logic is a special case of the logic of bunched implications (BI).

Separation logic facilitates reasoning about:

Separation logic supports the developing field of research described by Peter O'Hearn and others as local reasoning, whereby specifications and proofs of a program component mention only the portion of memory used by the component, and not the entire global state of the system. Applications include automated program verification (where an algorithm checks the validity of another algorithm) and automated parallelization of software.

Separation logic assertions describe "states" consisting of a store and a heap, roughly corresponding to the state of local (or stack-allocated) variables and dynamically-allocated objects in common programming languages such as C and Java. A store ${\displaystyle s}$ is a function mapping variables to values. A heap ${\displaystyle h}$ is a partial function mapping memory addresses to values. Two heaps ${\displaystyle h}$ and ${\displaystyle h'}$ are disjoint (denoted ${\displaystyle h\,\bot \,h'}$) if their domains do not overlap (i.e., for every memory address ${\displaystyle \ell }$, at least one of ${\displaystyle h(\ell )}$ and ${\displaystyle h'(\ell )}$ is undefined).

...
Wikipedia