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:
Automatic Function Annotations for Hoare Logic
speaker:
Daniel Matichuk
time:
Tuesday, 12 February 2013, 10:30am.
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:
Formal verification can provide a high degree of assurance for critical software, but can come at the cost of large artefacts that must be maintained alongside it. When using an interactive theorem prover, these artefacts take the form of large, complex proofs where the ability to reuse and maintain them becomes paramount. I will present my work on a function annotation logic, which is an extension to Hoare logic that allows reasoning on intermediate program states to be easily reused. Program functions are annotated with properties as a side-condition of existing proofs. These annotations can reduce the proof burden substantially when subsequent program properties need to be shown. Implemented in Isabelle, it is shown to be practically useful by greatly simplifying cases where existing proofs contained largely duplicated reasoning.
bio:
Daniel Matichuk obtained his B.Sc. in Honors Computer Science from the University of Alberta, Canada in 2011 and has since been working at NICTA in Sydney as a Research Engineer. He will soon be starting his PhD at NICTA and the University of New South Wales. His recent work was aiding in the noninterference proof for the seL4 microkernel and he is interested in maintenance and refactoring in large formal proofs.