9–11 Sept 2019
Europe/Lisbon timezone

Formal Methods for the Linux Kernel

10 Sept 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.
Diamond Sponsor

Platinum Sponsors



Gold Sponsors


Silver Sponsors

Evening Event Sponsor

Lunch Sponsor

Catchbox Sponsor

T-Shirt Sponsor

Official Carrier

Location Sponsor