Formal Methods for Kernel Hackers

Explore formal methods for kernel development in this 44-minute conference talk from the Linux Plumbers Conference. Discover how these tools, often perceived as academic and inaccessible, can be effectively used by kernel hackers to improve the Linux kernel. Learn about formal models that have uncovered real bugs in the kernel and discuss potential future applications, from modeling existing kernel implementations to formally specifying new design choices. Gain insights into PlusCal, an algorithm language based on TLA+, through introductory examples, with no prior knowledge required. Join speaker Catalin Marinas in demystifying formal methods and their practical applications in kernel hacking.