Un compilateur dédié à la transformation de programmes écrits en langage MinCaml vers du code assembleur ARM. Il permet de vérifier la cohérence des types, d'optimiser les performances et de générer un code exécutable pour des architectures matérielles cibles. Utilisé principalement dans un contexte académique ou de recherche pour l'enseignement des concepts de compilation.

Le projet Capla Compiler est une version modifiée du compilateur CompCert, un compilateur C formellement vérifié. Il permet de transformer du code source C en code assembleur pour différentes architectures matérielles (ARM, PowerPC, RISC-V, x86) tout en garantissant la conformité du code généré par rapport au code source. Ce projet est utilisé dans des contextes où la fiabilité et la sécurité des programmes compilés sont critiques, notamment dans les domaines de la recherche, de l'éducation et de l'industrie.

Chamois est un fork du compilateur C formellement vérifié CompCert, avec des ajouts de Verimag et Kalray. Il s'agit d'un compilateur pour un sous-ensemble important du langage C, générant du code pour les processeurs PowerPC, ARM, x86, RISC-V et KVX. La particularité de CompCert est qu'il a été prouvé correct à l'aide de l'assistant de preuve Coq : le code assembleur généré est garanti de se comporter comme prescrit par la sémantique du code C source.

Ce projet vise à reproduire des traces d'exécution de code sur un processeur ARM v7 en analysant les signaux générés par un analyseur logique. Il explore des attaques matérielles pour tromper un moniteur de sécurité en simulant des accès mémoire et des branchements indirects. Les résultats permettent de renforcer la sécurité des systèmes embarqués contre des attaques ciblant les mécanismes de traçage matériel.

CompCertSSA est une version étendue du compilateur C vérifié CompCert, avec un middle-end SSA pour la construction de la forme SSA, des optimisations SSA-based et des librairies associées. Il prend en charge un sous-ensemble important du langage C et génère du code assembleur pour PowerPC, ARM, x86 et RISC-V.