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
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:
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.