Linux Symposium

Toward Clustering the Kernel

Alexandre LISSY

Model-Checking techniques have a hard limit in term of number of states they can handle, even though new optimizations allows to go further and further. To be able to apply them on very large code base such as the Linux Kernel, we propose to slice it into parts that are manageable for Model-Checking ; a first step toward this achievement is studying the current kernel internal dependency topology.

Policies   |   Media Archives