CoqTL est un langage de programmation interne (DSL) pour la transformation de modèles dans l'environnement de preuve formelle Coq. Il permet de spécifier des transformations de modèles de manière déclarative et de générer des preuves pour ces transformations. Ce dépôt contient des exemples et des preuves pour CoqTL, ainsi que des générateurs pour créer des métamodèles et des modèles à partir de fichiers Ecore et XMI.

Le projet atsyra-dev vise à développer des plugins et un studio pour l'analyse de modèles formels, la transformation de langages spécifiques de domaines et la génération de code à partir de modèles. Il s'appuie sur des outils tels qu'Xtend, MapStruct, Testcontainers, OSGi, SLF4J, Entity Framework Core, Guava, OpenTracing, Simple Injector, Apache Ant et Markdown.

Outil académique dédié à la vérification compositionnelle de systèmes temps réel embarqués. Il permet de modéliser des tâches critiques, de générer des problèmes de programmation linéaire en nombres entiers (ILP) pour résoudre des contraintes d'affinité, et de traduire ces descriptions en modèles compatibles avec des outils de vérification formelle comme Uppaal. Utilisé pour des études de cas industrielles, notamment dans le domaine automobile.

OpenEmbedd est un projet dédié à la modélisation, la simulation et la génération de code pour les systèmes embarqués. Il permet de vérifier formellement des propriétés sur les modèles et facilite le développement de systèmes embarqués critiques.

Outil dédié à la traduction générique de théories dans le langage Dedukti, un système basé sur le λΠ-calcul modulo théorie. Il propose trois modèles de traduction : les morphismes de théorie, les relations logiques et les plongements de théorie. Ces fonctionnalités aident les utilisateurs à adapter des systèmes formels entre eux, facilitant ainsi la réutilisation et l'interopérabilité des preuves logiques.

PyXAI est une bibliothèque Python dédiée à l'IA explicable (XAI) pour les modèles d'apprentissage automatique basés sur des arbres (classification ou régression). Elle permet de générer des explications formelles, correctes et locales pour comprendre les décisions des modèles, tout en offrant des fonctionnalités de rectification pour corriger les incohérences entre les prédictions et les connaissances métier. L'outil s'adresse aux experts en data science et aux secteurs nécessitant une transparence accrue des algorithmes.

Outil dédié à la résolution de problèmes de satisfaction de contraintes (CSP) et à la validation de propriétés logiques sur des modèles formels. Il permet d'analyser des systèmes critiques en vérifiant leur cohérence et en générant des contre-exemples ou des preuves de validité. Développé dans le cadre d'un projet de recherche financé par l'ANR, il s'appuie sur des techniques avancées de logique et de satisfiabilité.

Outil dédié à la modélisation, l'analyse et la simulation de protocoles de sécurité pour les systèmes communicants. Il permet de générer des cas de test automatisés, d'identifier des vulnérabilités potentielles et de valider des propriétés de sécurité via des modèles formels. Utilisé principalement dans le domaine de la cybersécurité et de la vérification de systèmes.

Ce projet permet de simuler des systèmes à l'aide de modèles formels, de générer des modèles à partir de spécifications et d'analyser les comportements de ces systèmes.

MCsimCoq est un outil de simulation de systèmes de mémoire informatique. Il permet d'analyser les performances de différents types de mémoire, tels que DDR3 et DDR4, en utilisant des modèles formels générés par Coq. Il vérifie également la conformité des commandes de mémoire avec les protocoles spécifiés.