Ingredients of Operating System Correctness? Lessons Learned in the Formal Verification of PikeOS

Abstract. In the context of the Verisoft XT project functional correctness of the microkernel of PikeOS from SYSGO AG is shown at the source code level using the VCC verification tool, developed by Microsoft Research. In this paper we outline a simulation theorem between a top-level abstract model and the system consisting of the kernel and user programs running in alternation on the real machine. Based on an example of a typical code trace through the kernel, we identify the correctness properties of all components in the trace that are needed for the overall correctness proof of the microkernel.