Abstract

I’m developed a separation logic framework based on Abstract Separation Logic inside the HOL4 theorem prover. This framework is instantiated to build Holfoot, a formalisation of Smallfoot. In this talk, I will give a high-level presentation of Holfoot (http://holfoot.heap-of-problems.org).

Smallfoot
(http://www.dcs.qmul.ac.uk/research/logic/theory/projects/smallfoot)
is an automated separation logic tool. It is able to reason about the
partial correctness of programs written in a simple, low-level
imperative language, which is designed to resemble C. This language
contains pointers, local and global variables, dynamic memory
allocation/deallocation, conditional execution, while-loops and
recursive procedures with call-by-value and call-by-reference
arguments. Moreover, concurrency is supported by conditional critical
regions and a parallel composition operator.
Smallfoot-specifications are concerned with the shape of
datastructures in memory. Their content is not considered.

Holfoot can verify most Smallfoot examples completely automatically.
However, it extends Smallfoot to reason about the content of
datastructures. Moreover, there is support for arrays and pointer
arithmetic. Considering the data-content allows Holfoot to reason
about fully-functional specifications. Simple fully-functional
specifications like reversal of a single linked list can be verified
automatically. For more complicated examples like a fully-functional
specification of mergesort or insertion into a red-black-tree,
Holfoot can be used interactively inside HOL4. This allows using all
the libraries and tools of HOL4.

This talk will be a high-level presentation of Holfoot. I don't
expect the audience to be familiar with separation logic or HOL4. The
talk will briefly sketch the semantic foundations, i.e. Abstract
Separation Logic.  Then, an end-user view on Holfoot will be
presented. Holfoot's web-interface
(http://holfoot.heap-of-problems.org/web-interface.php) will be used
to run Holfoot on concrete examples.