Skip to main content


Lyrebird — assigning meanings to machines


David Cock




This paper presents work in progress on the Lyrebird framework, consisting of a language for specifying the programmer-visible behaviour of a processor and its associated devices, a tool for automatically producing a fast simulator, and a formal semantic interpretation providing a machine model for use in an interactive theorem prover. Machine specifications are modular, providing abstract interfaces and structural parameterization (MMU-less processors, for example). Also presented is a specific example: An instantiation for the ARM1136jf-s core.

BibTeX Entry

    publisher        = {USENIX},
    author           = {Cock, David},
    month            = oct,
    slides           = {},
    year             = {2010},
    title            = {Lyrebird --- Assigning Meanings to Machines},
    booktitle        = {Systems Software Verification},
    pages            = {1--9},
    address          = {Vancouver, BC, Canada }


Served by Apache on Linux on seL4.