Speaker
Catalin Marinas
Description
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 |
|---|
