Robin Micro-Hypervisor Specification and Verification

Documents

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

Software

• Olmar: An Ocaml framework for C++ AST manipulations
• memcheck: An Ocaml runtime type checking library
• ast2pvs: The semantics compiler [comming soon]
• pvs-status-smiley: Emacs lisp code to annotate PVS sources with proof status smilies

Home Science Overview All Publications Talks PhD CCSL Robin