Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
IMPORTANT: Please note that this talk is Monday.
- title: The L4.verified Project
- presenter: Dr. Gerwin Klein
- time: 10:30 am, 24 May 2010, Monday
- location
- Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
- abstract:
- Last year, the NICTA L4.verifed project produced a formal machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This talk will give an overview of the proof together with its main implications and assumptions, and will show in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security.
- bio:
- Dr Gerwin Klein is a Principal Researcher at NICTA and Conjoint Associate Professor at the University of New South Wales, Australia. He is working in the area of formal software verification, interactive theorem proving, and operating systems. He is the project leader of L4.verified. He received his PhD in 2003 from Technische Universitaet Munich on the topic of Java Bytecode Verification and has been working in the area of machine-checked formal proof in various projects since 1998.