Galois Tech Talk: Large Scale Monadic Refinement - Tales from L4.verified

[Don Stewart]

Next week's Galois Tech Talk:

------------------------------------------------------------------------

Title: Large Scale Monadic Refinement - Tales from L4.verified

Speaker: Thomas Sewell
NICTA

Date: **Wednesday** , August 27th, 10.30am

Location: Galois, Inc.
421 SW 6th Ave. Suite 300
(3rd floor of the Commonwealth Building)
Portland, Oregon

Abstract:

Components of operating systems have emerged as an attractive
target for formal analysis, thanks to the key importance of
operating system correctness in establishing the security of a
range of applications. These systems present a number of unique
challenges for analysis, including their low level implementation
and their detailed view of the system state. This talk will address
none of these, instead focusing on the challenges of reasoning
about (relatively) large, non-modular, inherently imperative
software artefacts.

The talk will describe the formalisation of the seL4 microkernel
using a state monad with nondeterminism and exceptions, present a
refinement and Hoare calculus, and discuss the impact of this
chosen approach on the effectiveness of the overall verification
effort.

Biographical details:

Thomas Sewell is a software engineer with an interest in pure
mathematics. He obtained his BE & BSc from UNSW in 2006, and has
been working as a proof engineer for NICTA's L4.verified project
for two and a half years.

About the Galois Tech Talks.

Galois (http://galois.com) has been holding weekly technical
seminars for several years 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. If you're planning to attend, dropping
a note to <do...@galois.com> is appreciated, but not required.
If you're interested in giving a talk, we're always looking for new
speakers.

------------------------------------------------------------------------