Outil de compilation et de gestion de builds dédié au langage MUMPS, un langage de programmation historique utilisé principalement dans le domaine médical. Il facilite l'automatisation des processus de compilation, la gestion des dépendances et l'intégration dans des pipelines de développement. Ce projet cible les développeurs travaillant sur des systèmes hérités ou des applications critiques nécessitant une maintenance rigoureuse.

Ce projet développe un serveur dédié pour les alimentations électriques Delta Elektronika. Il permet de réguler la puissance de sortie plutôt que la tension ou le courant, offrant ainsi une solution adaptée aux besoins spécifiques où la puissance constante est critique. Le serveur agit comme un intermédiaire entre l'utilisateur et l'alimentation, assurant une stabilité optimale du système.

TiAMo est un outil de vérification formelle dédié à l'analyse des systèmes temporisés modélisés par des automates temporisés. Il permet de vérifier des propriétés temporelles complexes sur des modèles, d'identifier des erreurs de conception ou de synchronisation, et d'optimiser des systèmes critiques comme les protocoles de communication ou les systèmes embarqués. Développé dans le cadre d'un projet de recherche, il est utilisé pour valider la correction et la fiabilité des systèmes avant leur déploiement.

LaREx est une solution innovante conçue pour détecter les décalages de distribution dans les données d'entrée des modèles d'intelligence artificielle, notamment ceux utilisés en vision par ordinateur. Elle permet d'évaluer la fiabilité des systèmes de classification d'images, de détection d'objets et de segmentation sémantique en identifiant les écarts entre les données d'entraînement et les nouvelles données. Développée par des chercheurs soutenus par des programmes publics français, cette méthode offre une approche légère et efficace pour renforcer la sécurité des applications critiques.

Outil dédié à l'analyse et à l'optimisation de modèles de compteurs abstraits utilisés en vérification formelle. Il permet de déterminer des tailles de ensembles concrets à partir de modèles pseudo-booléens, facilitant ainsi la validation de propriétés logiques complexes. Développé dans le cadre du projet BLaSST, il s'intègre dans des workflows de preuve automatisée pour les systèmes critiques.

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é.

Lustre est un système de fichiers distribué open source conçu pour gérer de grands volumes de données dans des environnements haute performance. Il permet de configurer, optimiser et maintenir des clusters de stockage pour des infrastructures critiques comme les centres de données ou les supercalculateurs. Le projet fournit des outils et des ressources pour faciliter le développement, le test et le déploiement de solutions de stockage distribué.

SWMB est un logiciel libre et modulaire conçu pour renforcer la sécurité des parcs informatiques sous Windows. Il permet aux administrations et organisations de déployer des configurations standardisées, automatiser des tâches critiques et garantir la conformité aux exigences de sécurité. Développé dans un cadre collaboratif, il s'appuie sur des bonnes pratiques éprouvées pour simplifier la gestion des systèmes tout en réduisant les risques liés aux vulnérabilités.

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.

Ouroboros est une bibliothèque développée par l'équipe TRACES de l'IRIT (Institut de Recherche en Informatique de Toulouse). Elle permet aux chercheurs de prototyper et d'expérimenter des modèles d'interférences dans l'ordonnancement statique des systèmes temps réel. L'outil facilite l'analyse et la validation de schedulers pour des applications critiques en informatique industrielle.