Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)
title: Towards a Formally Verified Component Platform
speaker: Matthew Fernandez
time: Tuesday, 16 October 2012, 10:30am
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
In safety- and security-critical environments software failures that are acceptable in other contexts may have expensive or even life-threatening consequences. Formal verification has the potential to provide high assurance for this software, but is regarded as being prohibitively expensive. Although significant advances have been made in this area, verification of larger systems still remains impractical. Component-based development has the potential to lower the cost of system-wide verification, bringing correctness proofs of these large scale systems within reach. This talk will discuss my work that aims to provide a component-based development environment for building systems with high assurance requirements. By providing a formal model of the platform with proven correctness properties that hold at the level of an abstract model right down to the implementation, I hope to reduce the cost of full system verification by allowing reasoning about system components in isolation.
bio: Matthew is a current PhD student at NICTA and the University of New South Wales, Australia. His research interests include kernel design, compilers, component systems and compiler implementation. His current work is aiming to provide formal guarantees for a component-based development environment on the seL4 microkernel.