The seL4 verification: the art and craft of proof and the reality of commercial support
The formal verification of the seL4 microkernel started as a research project in 2004 and has achieved commercial scale now, in the number of properties proven, the supported features and platforms, the adoption and deployment by industry and government organisations. It is supported by an open-source Foundation and a growing ecosystem. In this talk, I will reflect on the seL4 verification journey, past, present and future, and the challenges to combine the art and craft of proof with the reality of meeting industry demand for verified software.
June Andronick is CEO and co-founder of Proofcraft, providing commercial support, training, consulting, and contracted proof projects around software verification in general and the seL4 microkernel verification in particular. She is also CEO of the seL4 Foundation, and conjoint Associate Professor at UNSW. Her research focuses on increasing the reliability of critical software systems, by mathematically proving that the code behaves as expected and satisfies security and safety requirements. She previously led the Trustworthy Systems group, world-leading in the area of verified operating systems software, known worldwide for the formal verification of the seL4 microkernel. She was recognised in 2011 by MIT’s Technology Review as one of the world’s top young innovators (TR35). She holds a PhD in Computer Science from the University of Paris-Sud, France.
Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change
17:30 - 18:30
Invited TalkCPP at Salon III
Chair(s): Andrei Popescu University of Sheffield
|The seL4 verification: the art and craft of proof and the reality of commercial supportRemote|
I: June Andronick Proofcraft, UNSW and seL4 FoundationMedia Attached