Axe LCP

• Modèles de calcul : Cette thématique concerne l'études de différents modèles de calcul. Parmi les systèmes étudiés, on trouve les modèles de calcul à temps infinis, les transformations globales, le calcul naturel et plus...
• Complexité descriptive : Ce thème concerne la définissabilité dans divers logiques, souvent avec un aspect calculatoire explicite, que ce soit pour des aspects de décidabilité ou de complexité. Par exemple, le théorème plus...
• Aspects calculatoires des théories mathématiques : Nous nous intéressons aux fondements informatiques des mathématiques. D’une part, nous explorons les objets et les théories mathématiques au travers du prisme de leur complexité calculatoire, plus...
• Preuves et programmes : Les preuves et les programmes peuvent être considérés comme étant structurés par plusieurs opérations : a minima une opération de composition (d’une preuve de $A$ et de $A \Rightarrow B$, on plus...

Axe SVS

• Spécification de systèmes avec la méthode Event-B : Le cadre général des travaux du thème Spécification de systèmes avec la méthode Event-B concerne la spécification, la vérification et le développement de systèmes en utilisant des techniques plus...
• Parallélisme, calcul haute performance et applications : Le thème Programmation parallèle de haut-niveau et axé sur la conception de langages de haut-niveau pour la programmation parallèle, le design d’algorithmiques distribués et leur vérification plus...
• Systèmes hybrides, temporisés et stochastiques : Ce groupe de recherche se consacre à l’étude des méthodes et des modèles dédiés à l’analyse des systèmes hybrides, temporisés et stochastiques ou combinant ces aspects. Les travaux menés au sein plus...
• Méthodes formelles pour les transductions : L’étude des langages réguliers et leur correspondance avec les automates et différents formalismes logiques ont été appliquées avec succès à la vérification de programmes. On peut citer par plus...
• Synthèse et vérification des systèmes informatiques : La création des systèmes cybers-physiques est une tâche complexe, ceci est d'autant plus vrai quand il s'agit de systèmes critiques. Par exemple, une erreur logicielle dans le régulateur de plus...
• Logiques et modèles expressifs pour les systèmes multi-agents concurrents : a spécification et la vérification des propriétés des systèmes multi-agents se heurte à des barrières de complexité, voire même d’indécidabilité, car le problème de model-checking pour beaucoup plus...
• Modélisation et évaluation des performances de systèmes complexes : Ce thème concerne l’évaluation et l’analyse des performances dans les systèmes informatiques complexes, souvent avec un aspect formel et calculatoire explicite, que ce soit pour des plus...

Axe d'ouverture

• Droit du numérique : Les activités de recherche portent sur l'interaction entre la science informatique et le droit en action (parti du droit qui s'intéresse à l'exercice des droits). Les premières activités ont plus...