Formal Verification Made Easy - and Fast

Formal Verification Made Easy - and Fast

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.