Skip to main content


Formal system verification — extension, AOARD 114070


June Andronick, Gerwin Klein and Andrew Boyton




The AOARD project FA2386-11-1-4070 aims at providing a provably correct initialiser of componentised systems. Taking as input a description of the desired components, including the desired authorised communication between them, the initialiser sets up the system and provides a proof that the resulting concrete machine state of the system matches the desired authority state. Within the scope of this project, we provide (1) a formal specification of the initialiser, in terms of the steps needed to create the components and their communication channels; and (2) a formal proof that this specification is correct in that it either fails safely or produces the desired state.

The present document is an annual report of this project, presenting the status of the work undertaken so far. Namely, we have written the initialiser specification, we have set up a verification framework enabling modular reasoning and proofs, and we have progressed substantially on the proof.

BibTeX Entry

    author           = {Andronick, June and Klein, Gerwin and Boyton, Andrew},
    issn             = {1833-9646-5926},
    month            = may,
    year             = {2012},
    title            = {Formal System Verification --- Extension, {AOARD} 114070},
    institution      = {NICTA},
    address          = {Sydney, Australia}


Served by Apache on Linux on seL4.