Separation Logic

A logic for verification of programs with pointers. An extension of Hoare logic, uses bunched logic.

Concepts

Frame Rule

The frame rule states that a program satisfying the triple {P} C {Q} also satisfies {P ∗ R} C {Q ∗ R} (i.e. a program that executes properly in one heap context also executes correctly with the same result in any other larger heap context).

Tools