Separation logic is a formal logic for reasoning about programs, especially programs that manipulate memory and mutable data structures. It extends Hoare logic by making it possible to reason about separated portions of state and their safe composition.
An extension of Hoare logic, a way of reasoning about programs. The assertion language of separation logic is a special case of the logic of bunched implications (BI).