University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Looking Back at Lyrebird

Looking Back at Lyrebird

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity