#27 Formalizing an OS: The seL4 - Gerwin Klein
Type Theory Forall
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
Next Episodes
#26 Mechanizing Modern Mathematics - Kevin Buzzard @ Type Theory Forall
📆 2023-01-16 19:30 / ⌛ 02:15:31
#25 Formally Verifying the Tezos Codebase - Formal Land @ Type Theory Forall
📆 2022-11-21 15:05 / ⌛ 01:01:32
#24 The History of Isabelle - Lawrence Paulson @ Type Theory Forall
📆 2022-10-06 23:05 / ⌛ 01:38:02
#23 What is the SIGPLAN? - Jens Palsberg and Jonathan Aldrich @ Type Theory Forall
📆 2022-09-24 13:15 / ⌛ 01:13:05
#22 Impredicativity, LEM, Realizability and more - Cody Roux @ Type Theory Forall
📆 2022-08-12 17:15 / ⌛ 02:19:23