Modular Automatic Assertion Checking with Separation Logic

Separation logic is a program logic for reasoning about programs that
manipulate pointer data structures.
We describe a tool, Smallfoot, for checking certain separation logic
specifications.
The assertions describe the shapes of  data structures rather than their
detailed contents, and this allows reasoning to be fully automatic.
We illustrate what the tool can do via a sequence of examples which are
oriented around novel aspects of separation logic, namely:
avoidance of frame axioms (which say what a procedure does not change);
embracement of  ``dirty'' features such as memory disposal and address
arithmetic; information hiding in the presence of pointers; and modular
reasoning about concurrent programs.