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 |
