Sep 9 – 11, 2019
Europe/Lisbon timezone

Formal Methods for the Linux Kernel

Sep 10, 2019, 3:45 PM
Ametista/room-I (Corinthia Hotel Lisbon)


Corinthia Hotel Lisbon

Birds of a Feather (BoF) Birds of a feather (BoF)


Catalin Marinas


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

Primary author

Presentation materials

There are no materials yet.