WG211/M23Lawall

Towards Verification of Linux Kernel Code

Julia Lawall, Inria

There is a growing awareness that for critical infrastructure such as operating systems, more rigorous means of ensuring correctness are needed. Most previous efforts at operating system verification have considered operating systems for embedded systems, have created some form of model of the operating system code, or have designed the operating system from the ground up with verification in mind. In this talk we consider whether we can apply verification directly to the existing Linux kernel source code.

This is work in progress.

This is joint work with Keisuke Nishimura.