Formal Verification Made Easy - and Fast

This talk presents an event-based methodology for modeling complex Linux behavior with state machines, then translating models into efficient C code that runs in the kernel for verification. It also discusses extending the approach across kernel subsystems.

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