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!
- I assisted Makarius Wenzel with the 2014 Isabelle tutorial at the ENS. Makarius, amongst other things, developed the Isar language for structured proofs and the PIDE interface to Isabelle.
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
- on the project page,
- in the publication at ITP2014 and the related JAR2016 article,
- in the publication at ATVA2014, and,
- in the entries at the Archive of Formal Proofs on AWN and AODV.
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.