20-24 September 2021
US/Pacific timezone

Testing the Red-Black tree implementation of the Linux kernel against a formally verified variant

22 Sep 2021, 08:30
25m
Microconference2/Virtual-Room (LPC Virtual)

Microconference2/Virtual-Room

LPC Virtual

150
Testing and Fuzzing MC Testing and Fuzzing MC

Speakers

Mr Mete Polat (Technische Universität München) Lukas Bulwahn (Elektrobit Automotive GmbH)

Description

In this talk, we will show how to construct evidence of correctness through
testing and formal verification. In our case study, we test the long-standing
Red-Black tree implementation in the kernel against a variant in a functional
programming language. This variant has been formally verified in the interactive
theorem prover Isabelle [1]. To our surprise, the kernel Red-Black tree
implementation is a variant that is not known in the literature of functional
data structures so far. We are glad that we still found it to be correct with
newly identified invariants for the correctness proof.
[1] https://isabelle.in.tum.de/

I agree to abide by the anti-harassment policy I agree

Primary authors

Mr Mete Polat (Technische Universität München) Lukas Bulwahn (Elektrobit Automotive GmbH)

Presentation Materials