All the following code is additional material to the article of the
same name by the authors.
Reference [16] in the paper: the final version published in the ECEASST.
A newer and more complete version of the code is available here. It should also be maintained for the future versions of Coq.