Robin Micro-Hypervisor Specification and Verification

This page makes the results of work package 4 (Specification and Verification) of the Robin project available.


There are two deliverables describing the results in our work package, D12 and D13.
D12: Nova interface specification
This document is also available as technical report ICIS-R08011 of the ICIS department.
Download: [ps.gz] [ps] [pdf] [dvi.tar.gz]

D13: Nova micro-hypervisor verification
The real deliverable contains a main part (about 60 pages) and an 3000-page appendix containing pretty printed PVS sources and proofs. With minor modifications (deletion of references into the appendix) the main part is also available as technical report ICIS-R08012 of the ICIS department.

The huge appendix is there only for formal reasons. Don't download or print it. Download the PVS sources instead from the links below.

technical report: [ps.gz] [ps] [pdf] [dvi.tar.gz]

deliverable main part: [ps.gz] [ps] [pdf] [dvi.tar.gz]

deliverable 3000-page appendix: [ps.gz] [ps] [pdf] [dvi]

400-up version of the appendix (just 8 pages): [ps.gz] [ps] [pdf] [dvi]

PVS sources

Snapshot described in the above documents: [robin-hw-model-2008-05-15.tgz].


Home Science Overview All Publications Talks PhD CCSL Robin

last changed on 20 Sep 2011 by Hendrik