Nous nous intéressons aux méthodes de définition des sémantiques opérationnelles en recherchant des méthodes de description des comportements des programmes à l'exécution qui permettent de décrire de manière uniforme les comportements finis ou infinis. Nous les appliquons aux langages séquentiels, non-déterministes ou concurrents/parallèles et impératifs, fonctionnels, logiques, logiques avec contraintes, orientés objets, etc. Nous étudions les correspondances entre sémantiques et comprenons les autres sémantiques (dénotationnelles, relationnelles, axiomatiques, etc.) comme des approximations discrètes de la sémantique opérationnelle.
L'étude des méthodes de preuve de propriétés sémantiques de programmes est une étape intermédiaire dans notre démarche. Une preuve de correction est relative à une sémantique collectrice qui caractérise une classe de propriétés jugées intéressantes, comme par exemple les propriétés d'invariance ou de fatalité, pour résoudre un problème donné. La sémantique collectrice est en général une approximation discrète de la sémantique exacte où les propriétés jugées inintéressantes sont ignorées. L'approximation doit être correcte pour la classe de propriétés considérées (consistance) et peut être sans perte d'informations essentielles (complétude sémantique). Dualement, la sémantique collectrice peut être un raffinement de la sémantique standard où l'on ajoute des informations à la sémantique standard (comme les temps d'exécution) de manière compatible (la sémantique standard étant alors une approximation correcte de la sémantique collectrice). Notre travail porte sur les méthodes mathématiques (et en particulier logiques) de description des propriétés de programmes et de méthodes de preuve, la construction systématique de méthodes de preuve à partir de sémantiques collectrices, la conception de sémantiques collectrices pour des classes de propriétés et des langages particuliers.
L'analyse sémantique consiste à déterminer statiquement (à la compilation) et automatiquement (sans intervention humaine interactive) des propriétés dynamiques (à l'exécution) des programmes. Ces informations sont indispensables pour les compilateurs optimisants, les outils de transformation de programmes (comme les paralléliseurs pour les machines vectorielles ou massivement parallèles), les outils de test et vérification de programmes, etc.
Nous procédons par interprétation abstraite, c'est-à-dire par approximation discrète de la sémantique collectrice, cette fois-ci, avec perte d'information parfois essentielle (et ce pour faire face aux problèmes d'indécidabilité ou de trop grande complexité). Ceci conduit à étudier les structures mathématiques discrètes permettant d'exprimer les propriétés sémantiques approchées des objets manipulés par les programmes, et les méthodes de résolution itérative et approchée de systèmes d'équations de point fixe sur des ensembles ordonnés discrets (simplification, accélération de la convergence, etc.).