Le projet td3-au-dela-du-rationel est une plateforme dédiée à l'accompagnement thérapeutique, visant à aider les utilisateurs dans la compréhension de leurs rêves et la découverte de soi. Grâce à l'analyse de symboles et à l'exploration des émotions, cette plateforme souhaite offrir un espace d'expression et de réflexion, favorisant ainsi le bien-être et l'épanouissement personnel.

OATs'inside est un outil d'analyse qui manipule les applications Android natives. Le système utilise une approche hybride basée sur la surveillance dynamique et l'exécution symbolique basée sur des traces pour générer des graphes de flux de contrôle (CFG) pour chaque méthode de l'application analysée.

Ce projet fournit une sémantique de réécriture logique pour les automates temporels paramétriques avec variables globales (PTAV) et démontre que l'analyse de portée symbolique utilisant Maude-with-SMT est sound et complete pour le problème de portée des automates temporels. La théorie de réécriture peut également être utilisée pour la synthèse de paramètres.

PMC-SOG est un outil de vérification de modèles parallèles utilisant des graphes d'observabilité symbolique. Il permet de vérifier des propriétés temporelles sur des systèmes concurrents et distribués, de construire des graphes d'observabilité symbolique et d'analyser les performances de ces systèmes.

Le projet DM est dédié à l'analyse de documents textuels, avec une fonctionnalité clé de reconnaissance de symboles spécifiques. Il permet également de convertir des lettres en chiffres, offrant ainsi des outils utiles pour le traitement et l'interprétation de données textuelles.

Memetic Semantic Genetic Programming for Symbolic Regression est un projet open-source qui vise à optimiser des modèles mathématiques à l'aide de techniques de programmation génétique et de recherche de solutions approchées. Il permet d'analyser des données complexes et de trouver des solutions optimales ou sous-optimales en fonction des contraintes imposées.

Le projet sog-rop vise à fournir des outils pour l'analyse et la réduction de systèmes à événements partiels. Il permet de construire des graphes symboliques observables et de calculer des ensembles amples pour la réduction de modèles, contribuant ainsi à atténuer l'explosion d'état dans les systèmes concurrents.

Ce projet contient des scripts pour générer des benchmarks d'un papier de recherche. Il permet de comparer différents outils en analysant des graphes d'observations et en générant des chemins de test symboliques.

Le projet pta2maude fournit une sémantique en logique de réécriture pour les automates paramétriques en temps réel (PTAs) et montre que l'analyse de portée symbolique utilisant Maude-with-SMT est sound et complete pour le problème de portée des PTAs. Il inclut des benchmarks comparant nos méthodes avec Imitator.

WSymb est un outil d'analyse de la complexité temporelle des programmes informatiques. Il permet de calculer la durée d'exécution potentielle maximale d'un programme en générant des formules symboliques pour représenter les temps d'exécution.