Explore formal verification techniques for Linux in this conference talk from the Linux Plumbers Conference. Discover how to model complex Linux subsystems using automata-based methodologies, generate efficient C code from formal models, and run on-the-fly verification as efficiently as tracing. Learn about the potential for applying these techniques across various kernel subsystems, paving the way for a more formally verified Linux. Gain insights into overcoming the perceived complexity of formal modeling and verification, and understand how this approach can enhance Linux's reliability and correctness beyond traditional assertion-based methods.
Overview
Syllabus
Introduction
Linux is complex
Linux is critical
What do we expect from Linux
Test cases
What do we need
Models
Generics
Modeling
Tracing
State machines
Last year
State
Authority
Other verification methods
Restrictions
Blocking
Daniel
Taught by
Linux Plumbers Conference
