Looking Back at Lyrebird

Add to your list(s) Download to your calendar using vCal

• David Cock - NICTA and UNSW
• Wednesday 10 July 2013, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact magnus.myreen.

The Lyrebird framework for hardware simulators with formal semantics was developed during the L4.verified project, as an attempt to bridge the gap between the C language model and the underlying hardware, particularly for machine-management operations, such as cache flushing and page table switching. Lyrebird was initially presented at SSV 2010 .

As the scope of the overall project was curtailed, focussing sucessfully on the refinement between the abstract specification and the C language implementation, the Lyrebird work remained incomplete. What already exists is a DSL , together with compilers into both Isabelle/HOL and C, for specifying an interconnected processor architecture, including an ARM CPU core, a memory management unit, and a cache controller. This talk will explore whether this work might be combined with the more recent, and more complete, formalisations of the user-level semantics of the ARM instruction set: Particularly, whether they might be integrated to produce a sufficiently detailed machine model to support the verification of systems software.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.