BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Holfoot - a separation logic tool in HOL4 - Thomas Tuerk - Technis
 che Universität München
DTSTART:20120529T120000Z
DTEND:20120529T130000Z
UID:TALK38401@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:I'm developed a separation logic framework based on Abstract S
 eparation\n Logic inside the HOL4 theorem prover. This framework is instan
 tiated to\n build Holfoot\, a formalisation of Smallfoot. In this talk\, I
  will give a\n high-level presentation of Holfoot\n (http://holfoot.heap-o
 f-problems.org).\n\n Smallfoot\n (http://www.dcs.qmul.ac.uk/research/logic
 /theory/projects/smallfoot)\n is an automated separation logic tool. It is
  able to reason about the\n partial correctness of programs written in a s
 imple\, low-level\n imperative language\, which is designed to resemble C.
  This language\n contains pointers\, local and global variables\, dynamic 
 memory\n allocation/deallocation\, conditional execution\, while-loops and
 \n recursive procedures with call-by-value and call-by-reference\n argumen
 ts. Moreover\, concurrency is supported by conditional critical\n regions 
 and a parallel composition operator.\n Smallfoot-specifications are concer
 ned with the shape of\n datastructures in memory. Their content is not con
 sidered.\n\n Holfoot can verify most Smallfoot examples completely automat
 ically.\n However\, it extends Smallfoot to reason about the content of\n 
 datastructures. Moreover\, there is support for arrays and pointer\n arith
 metic. Considering the data-content allows Holfoot to reason\n about fully
 -functional specifications. Simple fully-functional\n specifications like 
 reversal of a single linked list can be verified\n automatically. For more
  complicated examples like a fully-functional\n specification of mergesort
  or insertion into a red-black-tree\,\n Holfoot can be used interactively 
 inside HOL4. This allows using all\n the libraries and tools of HOL4.\n\n\
 n This talk will be a high-level presentation of Holfoot. I don't\n expect
  the audience to be familiar with separation logic or HOL4. The\n talk wil
 l briefly sketch the semantic foundations\, i.e. Abstract\n Separation Log
 ic.  Then\, an end-user view on Holfoot will be\n presented. Holfoot's web
 -interface\n (http://holfoot.heap-of-problems.org/web-interface.php) will 
 be used\n to run Holfoot on concrete examples.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR