Formal Verification Made Easy and Fast

Learn about the practical applications of formal verification in Linux kernel development through this 32-minute conference talk. Explore how modeling parts of Linux, such as memory models and PREEMPT_RT synchronization, can be made accessible to developers. Discover a methodology based on Finite-State Machines using familiar tracing events, making formal verification more approachable. Gain insights into the challenges and benefits of modeling and verifying the Linux kernel, with a focus on runtime verification techniques that offer low overhead and often require no kernel modifications. Understand how these approaches can be applied to real-world scenarios, bridging the gap between theoretical formal models and practical day-to-day development in the Linux ecosystem.