Biography

Gernot has been building high-performance microkernels and microkernel-based operating systems for about 30 years. This includes the OKL4 microkernel which shipped on billions of Qualcomm modem chips, a kernel that runs on the Secure Enclave processor of iOS devices, and seL4 microkernel, the world's first OS kernel with a mathematical proof of implementation correctness. seL4, which won the 2023 ACM Software System Award, still has the most comprehensive mathematical assurance story of any non-toy OS kernel, and is still the only formally verified kernel with capability-based access control. It is deployed in critical systems around the world, aided by the seL4 Foundation which Gernot chairs. Electric car maker NIO has recently announced that their seL4-based SkyOS will ship in mass-production cars from 2024. Gernot is Scientia (distinguished) Professor at UNSW Sydney, a member of the German Academy of Science Leopoldina, and a Fellow of the Academy of the Australian Technology and Engineering (ATSE), the Royal Society NSW, the ACM, the IEEE, and Engineers Australia.

Presentations

Gernot Heiser