Institute for Computer Architecture
and Parallel Computing
Main page
Project overview
In this project, we aim at specifying an operating system kernel and formally verifying its correctness. The operating system kernel supports memory management without shared memory, I/O with devices, and process management, and synchronous interprocess communication.
Project status
We have developed the so-called CVM layer (communicating virtual machines) which encapsulates the hardware-dependent parts of the operating system kernel. Inline assembler code is needed only in the CVM layer. The VAMOS (verified architecture microkernel operating system) on top of this CVM layer is written completely in C0; its implementation is finished.
Project members
Dr. Jan Dörrenbächer
Ing. (it) Mauro Gargano
Dr. Mark A. Hillebrand
Dr. Thomas In der Rieden
M. Sc. Abdul Qadar Kara
Dr. Steffen Knapp
Dipl.-Ing. Dominik Rester
Yury Chebiryak
Anna Marchenkova