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'm rather addicted to working with ITPs—it's much more fun and far less error-prone to work with formal models inside such a system rather than just on paper!
Vélus: a formally verified Lustre compiler
Vélus is a compiler for a subset of Lustre and Scade that is specified in Coq (with some OCaml). It integrates the CompCert C compiler to define the semantics of machine operations (integer addition, floating-point multiplication, etcetera) and to generate assembly code for different architectures. The research challenges are
- to mechanize (i.e., put into Coq) the semantics of the programming constructs used in modern languages for Model-Based Development;
- to implement compilation passes and prove them correct;
- to interactively verify source programs and guarantee that the obtained invariants also hold of the generated code.
This project is a collaboration with Lélio Brun, Pierre-Évariste Dagand, Paul Jeanmaire, Xavier Leroy, Basile Pesin, Marc Pouzet, and Lionel Rieg.
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.