[Club2] Tue, July 29 talk by Thomas Sewell, Room: Turing (00.09.038)

[Johannes Hölzl]

Greetings,

On Tuesday, July 29, Thomas Sewell will visit us and give a talk on
checking the compiler, in the context of previous verification of the C
code.  Please note the unusual time and day of the week. 

Cheers, 
  Johannes

Thomas Sewell
======================================================================
Tue., July 10, 14:00, Room: Turing (00.09.38)


Verified software deserves a trustworthy compiler chain. It is
unfortunate that
software sometimes fails because of compilation errors, and doubly
unfortunate
if that software has been proven to be otherwise safe. Our project
investigates
one approach to this problem, by proving the correctness of binaries
compiled
with an off-the-shelf C compiler such as GCC.

Last year we reported that we had successfully proven compilation of the
verified seL4 kernel by GCC (4.5.1) at low levels of optimisation (-O1).
The
proof uses custom conversions in Isabelle/HOL and HOL4, with the heavy
lifting
done by SMT solvers. In this talk we give an overview of our previous
work and
discuss our a number of improvements we are working on. Firstly, we now
partially support higher optimisation levels. We have also made some
progress
towards replaying our proofs within the Isabelle/HOL theorem prover,
which will
allow us to check some SMT-based results we must currently trust. Proof
replay
has involved formalisation of the refinement logic underlying our
compilation
check, which involves a surprise appearance of the axiom of choice. We
will
finish this talk with a light discussion of the relationship between
choice and
infinite execution.

(Thomas Sewell is a PhD student at NICTA & UNSW, Sydney, Australia.
Before
getting involved in compiler proofs, he worked as a proof engineer for
the seL4
microkernel verification project.)