ADVENT: Architecture-Driven Verification ADVENT
of Systems Software

Formalisations in Coq

Several of our research results are formalised in the Coq theorem prover. This not only gives us extremely high confidence in the correctness of the results by ruling out the possibility of errors in the proofs, but also makes the results more easily extensible as one can build on our existing formalisations.

Soundness proofs

Weak memory models

Compositional compiler correctness