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