Recherches

L’équipe ACADIE a pour objectif de contribuer à l’amélioration des méthodes et outils de certification des logiciels distribués embarqués. Pour ce faire, ses thématiques de recherche se développent selon quatre axes complémentaires du plus théorique au plus applicatif :

• Cathégories et théorie des types
• Vérification : preuve, simulation, analyse statique
• Génération de code certifié
• Systèmes embarqués distribués et temps réel

Domaines de recherche (permanents et doctorants)

Permanents
Doctorants
Doctorants de ACADIEThéses en cours F. BarralDecidability of non-standard reductions in typed lambda-calculus.2008 S. Soloviev R. BouazizContributions aux Tests des Systemes Temps Réel Embarqués.2008 J.-P. Bodeveix, O. Koné A. BoukhrisValidation de transformations de programmes parallèles. J.-P. Bodeveix, C. Chaudet, M. Filali2010 B. Combemale TD ALI

Lire la suite

Développement et validation de méthodes

Un des buts de l’équipe est de développer des supports pour la production de logiciels certifiés.
Après nous être intéressés aux concepts fournis par des cadres logiques traditionnels tels que HOL, Coq et PVS ou des méthodes formelles telles que B, nous nous intéressons maintenant aux outils pour les systèmes réactifs et temps réel, tels que les langages d’architecture : AADL pour l’avionique et le spatial, les langages de transformation : ATL pour la transformation de modèles et plus (...)

Lire la suite

Modélisation et validation d’algorithmes répartis

La modélisation et la validation des algorithmes répartis se heurtent au nombre d’états possibles de tels systèmes, nombre souvent infini. Les méthodes de vérification par exploration exhaustive du domaine d’états sont alors impossibles. Face à ce problème, l’approche adoptée comporte deux aspects complémentaires :
d’une part, un effort de modélisation : il s’agit de définir des abstractions de haut niveau exprimant la répartition d’un calcul et/ou des données pour en simplifier (...)

Lire la suite

Théorie des types et de la démonstration

Nos travaux de recherche sont essentiellement centrés sur :
le lambda-calcul et la théorie des types,
la théorie de la démonstration dans des systèmes logiques non-classiques ,
les catégories munies de structure additionnelle,
les applications des méthodes de ces trois domaines en informatique.
Le lambda-calcul et la théorie de types sont utilisés dans une grande majorité des systèmes de preuve.
Nous nous intéressons actuellement au contenu calculatoire des théories de types qui contiennent les types (...)

Lire la suite