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.