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.

Spécification formelle pour la modélisation et la vérification de workflows sécurisés. Ce projet permet de définir des propriétés de sécurité à l'aide de la logique temporelle linéaire (LTL) et de les valider sur des modèles de tâches et de flux de données. Il s'appuie sur des outils de model checking pour garantir le bon fonctionnement et la sécurité des processus modélisés.

Automaton-ABC est une méthode statistique conçue pour estimer la probabilité de propriétés spatio-temporelles dans des modèles markoviens paramétriques de population. Ce projet permet d'analyser des systèmes biologiques ou physiques complexes en simulant leur comportement et en validant des hypothèses statistiques. Il s'appuie sur des outils mathématiques avancés pour fournir des résultats précis et exploitables dans le cadre de recherches théoriques ou appliquées.

Projet académique visant à analyser et comparer les performances et la sécurité des algorithmes cryptographiques face aux attaques par canaux auxiliaires. Il propose des outils pour évaluer les fuites temporelles et valider des propriétés de mémoire constante, notamment via des modes sécurisés (exposé, verrouillé, sans branchement, etc.). Les résultats sont générés sous forme de fichiers CSV pour faciliter l'analyse comparative.