This BoF session aims to bring together Linux kernel developers who have an interest in formal methods (or formal methods experts with an interest in kernel development). Topics for discussion:
- A poll of formal methods currently used in the context of the Linux kernel: SPIN, TLA+, CBMC, herd, plain English etc.
- High level design specification vs. low level algorithm modelling. What properties people seek to verify?
- Bridging the gap between formal models and the actual code: built-in run-time verification (e.g. lockdep), CBMC-based kernel self-tests, event trace analysis. Any other suggestions?
- How to encourage wider adoption of formal methods by kernel developers (e.g. help reduce the ramp-up time)
- Potential for a consolidated repository of formal specs (or in-kernel directory)
|I agree to abide by the anti-harassment policy||Yes|