On the Formal Foundation of a Verification Approach for System-Level Concurrent Programs
- Date and Time
Friday, August 20th, 2010 at 13:15
Polacksbacken, room 1145
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.