Formal Nova Interface Specification

Hendrik Tews, Tjark Weber, Erik Poll, Marko van Eekelen, and Peter van Rossum. Technical Report ICIS-R08011, Radboud University Nijmegen, May 2008.


This document contains one major result of work package 4 (kernel specification and verification) of the Robin project: a formal specification of the Nova interface. The specification consists of three main parts: (1) a definition of an abstract internal state for the Nova micro-hypervisor, (2) a description of the operations of the hypervisor in imperative pseudo-code that accesses and modifies the internal state, and (3) a combination of big-step denotational and small-step operational semantics to give semantics to the pseudo code as state modifying functions.


Also available at


  author      = {Tews, Hendrik and Weber, Tjark and Poll, Erik and Eekelen, Marko van and Rossum, Peter van},
  title       = {Formal {Nova} Interface Specification},
  number      = {ICIS--R08011},
  institution = {Radboud University Nijmegen},
  month       = may,
  year        = {2008}

Last modified: 2008-08-04