Verifications around the Linux KernelAlexandre LISSY
In this paper, we will present the current state of the art around the topic of verifying the Linux Kernel. However, we do not limit ourselves to only the Linux Kernel, but we also studied what has been done around other kernel, such as some work around OpenBSD, work from Microsoft, or work around the L4 Micro Kernel. We will talk about model checking techniques, bug-finding techniques, bug life tracking tools, and present some classification of the current state of the art to be able to have a clear view of what has been done, why, what has not been done, why, and what could be done and how. We will also study a specfic case of hand-done model checking of a small part of the Linux Kernel.