BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Looking Back at Lyrebird - David Cock - NICTA and UNSW
DTSTART:20130710T120000Z
DTEND:20130710T130000Z
UID:TALK45848@talks.cam.ac.uk
CONTACT:33478
DESCRIPTION:The Lyrebird framework for hardware simulators with formal sem
 antics was developed during the L4.verified project\, as an attempt to bri
 dge the gap between the C language model and the underlying hardware\, par
 ticularly for machine-management operations\, such as cache flushing and p
 age table switching. Lyrebird was initially presented at SSV 2010.\n\nAs t
 he scope of the overall project was curtailed\, focussing sucessfully on t
 he refinement between the abstract specification and the C language implem
 entation\, the Lyrebird work remained incomplete.  What already exists is 
 a DSL\, together with compilers into both Isabelle/HOL and C\, for specify
 ing an interconnected processor architecture\, including an ARM CPU core\,
  a memory management unit\, and a cache controller.  This talk will explor
 e whether this work might be combined with the more recent\, and more comp
 lete\, formalisations of the user-level semantics of the ARM instruction s
 et: Particularly\, whether they might be integrated to produce a sufficien
 tly detailed machine model to support the verification of systems software
 .
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR