Fichiers annexes du manuscrit

Preuves en Coq

Formalisation et preuve de la préservation du typage

• Documentation Coq / index
• Scripts de preuve Coq (archive.zip)

Formalisation et preuve du vérificateur d'horloges

• Documentation Coq / index
• Scripts de preuve Coq (archive .zip)

Formalisation et preuve de la méthode de calcul du WCET

• Documentation Coq / index
• Script de preuve Coq (fichier .v)

Fichiers de tests

Code des applications

• Carte perforée (archive .zip)
• Tempéreuse (archive .zip)
• Serpent (archive .zip)

Liens vers les logiciels

• OMicrob (Github)
• OCaLustre (Github)
• Bytecrawler (Github)