# An Outline of Separation Logic

## TL;DR

This paper introduces Separation Logic, an extension of Hoare Logic, designed to effectively reason about programs with pointers and aliasing issues, using new assertions and axioms to improve proof techniques.

## Contribution

It presents the formalization of Separation Logic with new assertions and axioms, demonstrating its application to pointer-manipulating programs and addressing aliasing problems.

## Key findings

- Separation Logic effectively handles aliasing in pointer programs.
- New assertions and axioms facilitate proofs of real pointer programs.
- Illustrative examples demonstrate the logic's unique features.

## Abstract

Separation Logic is an effective Program Logic for proving programs that involve pointers. Reasoning with pointers becomes difficult especially when there is aliasing arising due to several pointers to a given cell location. In this paper, we try to explore the problems with aliasing through some simple examples and introduce the notion of separating conjunction as a tool to deal with it. We introduce Separation Logic as an extension of the standard Hoare Logic with the help pf a programming language that has four pointer manipulating commands. These commands perform the usual heap operations such as lookup, update, allocation and deallocation. The new set of assertions and axioms of Separation Logic is presented in a semi-formal style. Examples are given to illustrate the unique features of the new assertions and axioms. Finally the paper concludes with the proofs of some real programs using the axioms of Separation Logic.