BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verified LISP implementations on ARM\, x86 and PowerPC / A HOL For
 malisation of Smallfoot - Magnus Myreen &amp\; Thomas Tuerk
DTSTART:20090812T120000Z
DTEND:20090812T130000Z
UID:TALK19309@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Magnus Myreen and Thomas Tuerk are going to practice their TPH
 OLS talks. So\, there will be two 20 minute talks.\n\n\nMagnus Myreen:\nVe
 rified LISP implementations on ARM\, x86 and PowerPC\n\nThis paper reports
  on a case study\, which we believe is the first to produce a formally ver
 ified end-to-end implementation of a functional programming language runni
 ng on commercial processors.  Interpreters\nfor the core of McCarthy's LIS
 P 1.5 were implemented in ARM\, x86 and PowerPC machine code\, and proved 
 to correctly parse\, evaluate and print LISP s-expressions.  The proof of 
 evaluation required working on top of verified implementations of memory a
 llocation and garbage\ncollection.  All proofs are mechanised in the HOL4 
 theorem prover.\n\n\nThomas Tuerk\nA Formalisation of Smallfoot in HOL\n\n
 I'm building a framework based on Abstract Separation Logic in HOL. Furthe
 rmore\, I use this framework to build a tool called Holfoot that is simila
 r to Smallfoot. In this talk I will give a high level presentation of the 
 framework and especially Holfoot.\n\nSmallfoot is one of the oldest and be
 st documented separation logic tools. It is able to automatically prove sp
 ecifications about programs written in a simple\, low-level imperative lan
 guage. This programming language is designed to be similar to C. It contai
 ns pointers\, local and global variables\, dynamic memory allocation/deall
 ocation\, conditional execution\, while-loops and recursive procedures wit
 h call-by-value and call-by-reference arguments. Moreover\, there is suppo
 rt for parallism.\n\nHolfoot is able to parse Smallfoot-specifications and
  verify them automatically inside HOL. While Smallfoot-specifications only
  talk about the shape of data-structures in memory\, my tool is able to re
 ason about their data-content as well. However\, proofs of fully-functiona
 l specification usually need user interaction.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR