Galois Tech Talks

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.

# vimeo.com/61646976 Uploaded 205 Plays / / 0 Comments Watch in Couch Mode

Galois Tech Talks

Galois Video Plus

This channel contains video from the tech talks presented by galois.com

Galois has been holding weekly technical seminars since 2006 on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating


+ More

This channel contains video from the tech talks presented by galois.com

Galois has been holding weekly technical seminars since 2006 on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free.

Each week new tech talks are published at galois.com/blog/category/techtalks/ and you can find out about upcoming talks on twitter.com/galoisinc

Browse This Channel

Shout Box

Channels are a simple, beautiful way to showcase and watch videos. Browse more Channels. Channels