Galois Inc. Tech Talk: Experiences in a decade of maintaining and extending the seL4 proofs

Speaker:

June Andronick, Principal Research Scientist at Data61|CSIRO

Abstract:

Our formally verified microkernel, seL4, is now used across the world in a number of applications that keeps growing. In this talk, we will share our experience in maintaining and extending a successfully deployed verified software artifact for more than a decade, and some of the approaches we have developed to address the challenges of verifying an evolving implementation.

Bio:

June Andronick leads the Trustworthy Systems group, world-leading in verified operating systems software, known worldwide for the formal verification of the seL4 microkernel. She is a Principal Research Scientist at Data61|CSIRO, and conjoint Associate Professor at UNSW Sydney, Australia.

proofs