#27 Formalizing an OS: The seL4 - Gerwin Klein
Type Theory Forall
English - February 04, 2023 22:45 - 1 hour - 80.5 MB - ★★★★★ - 6 ratingsTechnology Science type theory programming languages academia Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: #26 Mechanizing Modern Mathematics - Kevin Buzzard
Next Episode: #28 Formally Verifying Smart Contracts - Pruvendo
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