BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Formalisation of Finite Automata in Isabelle/HOL - Thomas Tuerk 
 (University of Cambridge)
DTSTART:20130212T130000Z
DTEND:20130212T140000Z
UID:TALK43287@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:As part of the CAVA project (http://cava.in.tum.de)\, I develo
 ped a library for finite automata in Isabelle/HOL.  This library provides 
 high-level\, abstract definitions as well as low-level\, executable ones. 
 The first part of this talk will give an overview of this library. Then\, 
 a Presburger Arithmetic-case study will be used to demonstrate\, how the l
 ibrary can be used. Finally\, the implementation of Hopcroft's algorithm w
 ill be discussed in detail.\n\nThis talk was originally sheduled for 23rd 
 October 2012\, but cancelled due to illness.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR