This repository hosts supplementary material for the paper: the full Coq formalisation and the verified case study.
Submitted to ESOP'19.
This work is partially supported by the NWO VICI 639.023.710 Mercedes project and by the NWO TOP 612.001.403 VerDi project.