#27 Formalizing an OS: The seL4 - Gerwin Klein

Type Theory Forall

• Episode: #27 Formalizing an OS: The seL4 - Gerwin Klein
• Website: Type Theory Forall
• Feed URL: https://www.typetheoryforall.com/episodes.mp3.rss
• Duration: 01:58:40
• Published: 2023-02-04 21:45

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

• Gerwin’s Twitter
• Gerwin’s Website
• ProofCraft’s Website