BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A HOL Formalisation of Smallfoot - Thomas Tuerk (University of Cam
 bridge)
DTSTART:20090127T130000Z
DTEND:20090127T140000Z
UID:TALK16353@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:In my last ARG Lunch talk I presented a formalisation of Abstr
 act Separation Logic in HOL. Based on this formalisation\, I build a forma
 lisation of a tool similar to Smallfoot. This talk will present this tool 
 and\nits formalisation.\n\nSmallfoot is one of the oldest and best documen
 ted separation logic tools. It is able to automatically prove specificatio
 ns about programs written in a simple\, low-level imperative language. Thi
 s programming language is designed to be similar to C. It contains pointer
 s\, 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\, there is support for par
 allism. \n\nMy tool is able to parse Smallfoot-specifications and verify t
 hem automatically inside HOL. While Smallfoot-specifications only talk abo
 ut the shape of data-structures in memory\, my tool is able to reason abou
 t their data-content as well. However\, proofs of fully-functional specifi
 cation usually need user interaction.\n\n\nThe talk will consist of 3 part
 s. First\, I will shortly present the theoretical background and give an o
 verview over the Smallfoot formalisation. Then I will give a demonstration
  on how a fully-functional-specification of mergesort can be proved using 
 the tool. After this\, there will be time for questions and people that ar
 e not interested in HOL implementation details will be able to leave. \nFi
 nally\, I plan to give an overview over some general HOL infrastructure th
 at I developed for this tool. This part of the talk will require some know
 ledge of HOL and might only be of interest to HOL-users. In particular\, I
  will present consequence conversions (/src/bool/ConseqConv) and the quant
 ifier instantiation-heuristics library (/src/quantHeuristics). \n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR