Holfoot - a separation logic tool in HOL4

Add to your list(s) Download to your calendar using vCal

• Thomas Tuerk - Technische Universität München
• Tuesday 29 May 2012, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact William Denman.

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.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.