Sep 20 – 24, 2021
US/Pacific timezone

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

Sep 22, 2021, 8:30 AM
Microconference2/Virtual-Room (LPC Virtual)


LPC Virtual

Testing and Fuzzing MC Testing and Fuzzing MC


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


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.

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

Diamond Sponsor

Platinum Sponsor

Gold Sponsors

Silver Sponsors

Speaker Gift Sponsor

T-Shirt Sponsor

Conference Services provided by