On the Formal Foundation of a Verification Approach for System-Level Concurrent Programs

Abstract: Though program verification is known for and used since decades, the pervasive verification of a complete computer system still remains a grand challenge. In essence, this challenge stems from the interaction of various programs. Different techniques have been proposed for the verification of communicating programs. Common to all, however, is that they rely on assumptions about the underlying system. Typically, such assumptions include compiler correctness, scheduler fairness, and a certain non-interference between the local program behavior and its environment. I discharged these assumptions for the processes of a microkernel, called VAMOS. With my result, I formally justify the abstraction from a kernel model with explicit, deterministic scheduling to a concurrent process system with non-deterministic but temporally fair scheduling.