LoVe: Logique et Vérification

Le 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:

• théorie de la démonstration et lambda-calcul:
  la correspondance de Curry-Howard est fondamentale dans notre vision de la logique. Sous cette perspective, notre modèle de calcul privilégié est le lambda-calcul, que l’on peut voir comme le langage fonctionnel prototypique. Une place importante est jouée aussi par la logique linéaire, vue comme source de méthodologie et d’outils pour l’analyse de programmes, notamment à travers les formalismes de démonstration/calcul graphiques issus de celle-ci (réseaux de prevue, réseaux de partage…). La perspective Curry-Howard est aussi à la base de la formalisation et automatisation de preuves développé au sein de l’équipe, notamment en Coq.
• logique et modèles de ressources de calcul:
  L’intérêt vers les aspects quantitatifs dans les langages de programmation (analyse statique de ressources, probabilité, calcul quantique) s’est considérablement accru ces dernières années. Notre équipe s’attaque à ce type d’analyse avec les modèles issus de la logique linéaire, et en particulier de sa variante différentielle, parcimonieuse et de la géométrie de l’interaction. Une thématique importante ici est la complexité implicite, c’est-à-dire l’étude des classes de complexité à travers des méthodes logiques.

Les 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:

• Conception de spécifications formelles: le développement des spécifications est une tâche délicate, et il est facile de faire des erreurs. Le cadre des spécifications formelles oblige à une meilleure précision, et est ici sous-jacent aux travaux qui choisissent une expression en diagrammes UML.
• Vérification paramétrée, modulaire et distribuée: la conception de nouvelles techniques de vérification permettant de combattre le problème de l’explosion combinatoire constitue un axe majeur de nos recherches.
• Sûreté et sécurité logicielles: l’analyse de programmes concurrents est encore balbutiante. Nous étudions différents formalismes pour modéliser les programmes récursifs parallèles, et des techniques d’analyse associées. Nous développons aussi différents modèles pour la détection de malware et la découverte de comportements malveillants.