Ce plugin permet d'analyser et d'optimiser les caches de type LRU (Least Recently Used) dans le cadre de l'outil Otawa, dédié à l'analyse statique de programmes. Il fournit des métriques précises pour évaluer l'efficacité des politiques de cache et améliorer les performances des systèmes logiciels ou embarqués. Utilisé principalement dans le domaine de la recherche académique et de l'ingénierie 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.

Ce projet développe une solution innovante de reconnaissance de gestes et d'activités humaines basée sur des radars millimétriques. Il propose une méthodologie légère et robuste pour des systèmes embarqués, exploitant des réseaux de neurones graphiques (GNN) afin d'analyser des données radar complexes. Le projet inclut la création d'un jeu de données dédié, MIRAGE, et démontre une performance supérieure aux méthodes existantes en termes de précision et d'efficacité énergétique.

VeriFast est un outil d'analyse statique conçu pour vérifier la sécurité et la correction des programmes. Il permet de détecter des vulnérabilités potentielles dans le code source, notamment en Java, en s'appuyant sur des annotations et des propriétés formelles. L'outil est utilisé pour garantir la robustesse des systèmes critiques, comme les cartes à puce ou les applications embarquées, en identifiant les erreurs de logique ou les failles de sécurité avant leur déploiement.

Outil formel dédié à l'analyse de la robustesse des systèmes embarqués face aux attaques par injection de fautes. Il combine la description RTL d'un processeur, le binaire d'un logiciel et un modèle d'attaquant pour évaluer la sécurité d'un système intégrant des contre-mesures. µArchiFI permet de prouver formellement la sécurité d'un système ou d'identifier des contre-exemples illustrant des vulnérabilités exploitables.

Ce projet développe un système embarqué de classification automatique des sons urbains pour mesurer et analyser la pollution sonore. À partir d'enregistrements audio de dix secondes, il identifie huit types de sources sonores (moteurs, machines, voix humaines, etc.) et permet aux autorités municipales de mieux cibler leurs actions contre les nuisances sonores. Le système est conçu pour être déployé sur des capteurs connectés dans une ville, offrant une surveillance continue et objective des niveaux de bruit.

Outil open source dédié à l'optimisation et à la synthèse de haut niveau (HLS) pour les circuits électroniques. Il permet de transformer des descriptions algorithmiques en architectures matérielles optimisées, facilitant ainsi la conception de systèmes embarqués et de circuits intégrés. Le projet intègre des fonctionnalités avancées pour l'analyse de performance et la génération automatique de code VHDL ou Verilog.

VeriFast est un outil d'analyse statique formelle conçu pour vérifier la correction de programmes écrits en C et Java. Il permet de détecter des erreurs de typage, des violations de propriétés de sécurité et des bugs potentiels avant l'exécution. Utilisé principalement dans les domaines critiques comme les systèmes embarqués ou les applications sécurisées, il aide les développeurs à prouver que leur code respecte des spécifications formelles.

Outil spécialisé dans l'analyse précise des caches LRU (Least Recently Used) pour optimiser les performances des systèmes embarqués ou des applications critiques. Il permet de détecter des anomalies dans la gestion mémoire, d'identifier des fuites potentielles et d'améliorer l'efficacité des algorithmes de cache. Utilisé principalement par des développeurs et des ingénieurs en optimisation logicielle.

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.