Model Checking the Linux Kernel ?

Some people are trying to find defects in the code by searching for known patterns and known misuse, documented either as part of the kernel API usage or after bugs being known. At Mandriva, and as foundation of my PhD subject, we want to explore another way which is well-known but complex: Model-Checking. Main goal of this talk will be to introduce the subject and present the state of the art around kernel code checking