| Théses en cours |
| F. Barral | Decidability of non-standard reductions in typed lambda-calculus. | 2008 |
| | S. Soloviev | |
| R. Bouaziz | Contributions aux Tests des Systemes Temps Réel Embarqués. | 2008 |
| | J.-P. Bodeveix, O. Koné | |
| A. Boukhris | Validation de transformations de programmes parallèles. | |
| | J.-P. Bodeveix, C. Chaudet, M. Filali | 2010 |
| B. Combemale | Sémantique d’exécution et Ingénierie Dirigée par les Modèles : | juin 2008 |
| | application à l’Ingénierie des Procédés | |
| | X. Crégut, M. Pantel, X. Thirioux | |
| A. El Khoury | Etude de la commutativite des diagrammes categoriques | |
| | et calcul formel. | |
| | S. Soloviev, M. Spivakovski |
| P.-L. Garoche | Analyse Statique d’applications embarquées réparties. | juin 2008 |
| | M. Pantel, X. Thirioux | |
| N. Izerrouken | Vérification et validation formelle d’un | |
| | générateur de code embarqué temps réel. | fin 2009 |
| | M. Gandriau, M. Pantel, M. Strecker, X. Thirioux | |
| T. Le Berre | Validité temporelle des données dans les systèmes embarqués distribués | fin 2009 |
| | P. Mauran, G. Padiou, P. Quéinnec | |
| L. Marie-Magdeleine | Lambda termes inversibles et traitement dínformations | |
| | S. Soloviev | |
| Lei Pi | Vérification dans les langages d’architecture. | |
| | J.-P. Bodeveix, M. Filali, M. Strecker | fin 2009 |
| N. Pontisso | Vérification formelle des aspects temporels dans les | fin 2009 |
| | architectures logicielles à composants | |
| | P. Mauran, G. Padiou, P. Quéinnec | |
| M. Rebout | Récriture de graphes | |
| | L. Féraud, S. Soloviev | |
| J.-F. Rolland | Sémantique formelle des mécanismes architecturaux. | fin 2008 |
| | Application à AADL. | |
| | J.-P. Bodeveix, M. Filali | |
| Théses soutenues |
| J. Brunel | Combinaison des logiques temporelles et déontiques pour la | 2007 |
| | spécification de politiques de sécurité. | |
| | J.-P. Bodeveix, M. Filali | |
| C. Cubat dit Cros | Agents Mobiles Coopérants pour les Environnements Dynamiques | 2005 |
| | P. Mauran, G. Padiou, P. Quéinnec | |
| L. Méhats | Théorie de la preuve des catégories monoïdales symétriques fermées : | 2005 |
| | cohérence et équivalences de dérivations | |
| | S. Soloviev |
| O. Nasr | Spécification et Vérification des ordonnanceurs temps réel en B. | 2007 |
| | J.-P. Bodeveix, M. Filali | |
| M. Rached | Spécification et vérification des systèmes temps réel réactifs en B. | 2007 |
| | J.-P. Bodeveix, M. Filali | |