Le projet cv2fstar-material est un dépôt de code source contenant une extension pour l'outil CryptoVerif, qui permet de vérifier la correction et la sécurité des protocoles cryptographiques. Cette extension, développée dans le cadre d'une thèse de doctorat, permet de générer automatiquement du code sécurisé à partir de spécifications formelles, améliorant ainsi l'efficacité et la fiabilité du processus de développement de protocoles cryptographiques.

Outil open source dédié à l'identification automatique des vulnérabilités CVE (Common Vulnerabilities and Exposures) dans les codes sources. Il permet aux développeurs et équipes de sécurité de scanner leurs projets pour détecter des failles connues, analyser les correctifs associés et comprendre les modifications nécessaires pour sécuriser leur code. Le projet combine des analyses statiques via des requêtes Tree-sitter et des outils de traitement de données pour générer des jeux de données exploitables.

Bibliothèque d'outils pour simplifier et standardiser la création de fichiers CMakeLists.txt. Elle propose des modules pour gérer automatiquement les chemins d'installation, les RPATH, et la génération de fichiers de configuration pour les dépendances. Ces outils permettent aux développeurs de se concentrer sur le code métier tout en assurant une intégration fluide des bibliothèques et exécutables dans des projets CMake, qu'ils soient autonomes ou intégrés comme sous-projets.

Outil permettant d'automatiser la comparaison de valeurs de variables entre deux exécutions de programmes Fortran. Il injecte du code pour tracer les valeurs des variables et génère des rapports détaillés sur les différences détectées. Idéal pour identifier les causes de divergences dans des simulations ou des calculs scientifiques, facilitant ainsi le débogage et la validation de modèles.

Outil dédié à la génération automatique de code à partir de modèles de machines à états finis. Il permet aux développeurs de concevoir des systèmes logiciels complexes en définissant des états, transitions et événements, puis en produisant le code source correspondant. Idéal pour les applications nécessitant une modélisation comportementale précise, comme les interfaces utilisateur ou les systèmes embarqués.

Outil dédié à la génération automatique de parseurs et générateurs de code à partir de grammaires définies. Il simplifie la création d'analyses syntaxiques pour des langages spécifiques, réduisant ainsi le temps de développement des compilateurs et outils d'analyse. Idéal pour les développeurs et équipes travaillant sur des projets nécessitant une manipulation avancée de langages formels.

Outil web dédié à la génération automatique de code pour le simulateur CLASS, utilisé principalement dans le domaine de la modélisation et de la simulation de scénarios industriels complexes. Il permet aux utilisateurs de configurer des simulations, de créer des modèles, des réacteurs et des unités de production (comme des stocks ou des usines de séparation) via une interface graphique intuitive. Le projet facilite l'intégration de nouvelles fonctionnalités ou types d'unités en étendant les formulaires et la logique de génération de code.

Catala est un langage de programmation dédié à la rédaction et à l'analyse de textes législatifs. Il permet de définir des règles complexes de manière claire et précise, et de générer automatiquement du code à partir de ces règles. Catala vise à améliorer la fiabilité et la transparence des systèmes législatifs en automatisant certaines tâches de vérification et de mise en œuvre.

AutoJMH est un outil qui prend en entrée un segment de code et une exécution d'entraînement, et génère un microbenchmark JMH complet pour le segment. L'outil génère la classe JMH et place le segment de code à l'intérieur de la méthode wrapper, générant entièrement le microbenchmark. AutoJMH initialise également les variables du microbenchmark et effectue une série d'analyses pour éviter automatiquement les pièges courants de la microbenchmarking.

Dx est un outil permettant de dériver automatiquement du code C à partir de code Gallina monadique, proche du code C final. Il facilite la conversion de définitions formelles en code exécutable en générant une représentation intermédiaire puis un module C compilable. Principalement utilisé dans le domaine de la vérification formelle et des compilateurs, il s'intègre avec des outils comme CompCert pour produire du code C optimisé et vérifié.