Linux and Formal Methods

I’ve been working with the application of formal methods on Linux during my Ph.D. The idea is to formally model the behavior of Linux (what do expect from Linux?) and to verify and monitor Linux execution (is Linux behaving as expected?)

In the Linux Task Model page, you can find mode about modeling part of the Linux Behavior

In the Efficient Formal Verification for the Linux Kernel page, you can find more about the runtime monitoring of automata-based models for Linux.