Department of Information Technology

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

Speaker

Matthias Daum

Date and Time

Friday, August 20th, 2010 at 13:15

Location

Polacksbacken, room 1145

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.

Back to the seminar page

Updated  2010-08-16 13:40:44 by Frédéric Haziza.