Responsable Damiano Mazza
Notre équipe est structurée en deux axes de recherche, menant leurs activités de manière autonome :
- Types, modèles et théorie de la programmation ;
- Spécification et vérification modulaires et distribuées.
Consulter le rapport d’équipe 2012-2017 pour des informations plus détaillées.
Types, modèles et théorie de la programmationResponsable: Damiano MazzaLe trait d’union de cette sous-équipe est l’utilisation de techniques et outils de nature logique pour l’analyse, le développement et la formalisation de programmes. Nous attachons une importance particulière à l’étude fondationnel des aspects quantitatifs de programmes, comme la complexité (temps, espace), les comportements probabilistes et la formalisation de l’analyse réélle, ainsi que la modélisation du non-déterminisme et de la concurrence. Nos recherches couvrent aussi la modélisation du langage naturel et le raisonnement temporel.
Nous pouvons regrouper nos recherches en deux thématiques principales:
|
Spécification et vérification modulaires et distribuéesResponsable: Kaïs KlaiLes systèmes développés de nos jours sont de plus en plus complexes et leur fonctionnement peut avoir des conséquences importantes sur leur environnement, voire irréversibles : systèmes avioniques, médicaux… Il est par conséquent indispensable de garantir des systèmes sûrs, dont le fonctionnement a pu être vérifié avant leur mise en oeuvre. L’écriture d’une spécification formelle permet non seulement une meilleure compréhension du système étudié, mais aussi de prouver formellement, par une vérification exhaustive, son bon fonctionnement, quelle que soit l’exécution du système.
Nos activités s’articulent autour de trois principales thématiques de recherche:
|