ADVENT: Architecture-Driven Verification ADVENT
of Systems Software

Verified Compilation for Sequential Programs

We have constructed three verified compilers, which are implemented and verified in the Coq proof assistant.

The source code for these compilers is available at the links above.

Compilation under Weak Memory Models

We have also studied the correctness of compilation under weak memory models. Specifically: