9-11 September 2019
Europe/Lisbon timezone

Formal Methods for the Linux Kernel

10 Sep 2019, 15:45
45m
Ametista-room-I (Corinthia Hotel Lisbon)

Ametista-room-I

Corinthia Hotel Lisbon

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

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

Primary author

Presentation Materials

There are no materials yet.
Your browser is out of date!

Update your browser to view this website correctly. Update my browser now

×