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)
