PLAY PODCASTS
#27 Formalizing an OS: The seL4 - Gerwin Klein

#27 Formalizing an OS: The seL4 - Gerwin Klein

Gerwin Klein

Type Theory Forall

February 4, 20231h 58m

Audio is streamed directly from the publisher (api.typetheoryforall.com) as published in their RSS feed. Play Podcasts does not host this file. Rights-holders can request removal through the copyright & takedown page.

Show Notes

In this episode talk with Gerwin Klein about the formal verification of the microkernel seL4 which was done using Isabelle at NICTA / Data61 in Australia. We also talk a little about his PhD Project veryfing a piece of the Java Virtual Machine.

Links