Interactive Theorem Proving

I was fortunate to work in the theorem proving group of Gerwin Klein at NICTA (now Data61) in Sydney where the Isabelle interactive theorem prover (ITP) is applied to the verification of embedded systems code. Ever since I am rather addicted to working with ITPs—it is much more fun (and far less error-prone) to work with formal models inside such a system rather than just on paper!

Invariant proofs of network protocols (AWN and AODV)

Peter Höfner, Rob van Glabbeek, and I mechanized (i.e., put into Isabelle) the Algebra for Wireless Networks (AWN) and developed an associated framework for compositional proofs of safety properties. We applied this work to mechanize a proof of loop freedom of the AODV routing protocol for wireless mesh networks. Details can be found

The seL4 microkernel and proofs

I contributed to the seL4 microkernel and proofs in the L4.verified project (and afterward). Some details are in the publications on large-scale proofs and information flow enforcement. Otherwise, I presented an overview of the project in the course on Systems and Networks at the ENS.