Mechanized verification of the correctness and asymptotic complexity of programs : the right answer at the right time
Vérification mécanisée de la correction et complexité asymptotique de programmes
par Armaël GUENEAU sous la direction de François POTTIER et de Arthur CHARGUÉRAUD
Thèse de doctorat en Informatique
ED 386 Sciences Mathematiques de Paris Centre

Soutenue le lundi 16 décembre 2019 à Université Paris Cité

Sujets
  • Algorithmes
  • Assistants de preuve
  • Logique informatique
  • Méthodes formelles (informatique)

Les thèses de doctorat soutenues à Université Paris Cité sont déposées au format électronique

Consultation de la thèse sur d’autres sites :

TEL (Version intégrale de la thèse (pdf))

Description en anglais
Description en français
Mots clés
Preuves formelles, Complexité asymptotique, Logiques de programme, Logique de séparation
Resumé
Cette thèse s'intéresse à la question de démontrer rigoureusement que l'implantation d'un algorithme donné est non seulement correcte (elle renvoie bien le bon résultat dans tous les cas possibles), mais aussi possède la bonne complexité asymptotique (elle calcule toujours ce résultat en le temps attendu).Pour les chercheurs en algorithmique, caractériser la performance d'un algorithme se fait généralement en indiquant sa complexité asymptotique, notamment à l'aide de la notation "grand O" due à Landau. Nous détaillons, tout d'abord informellement, pourquoi de telles bornes de complexité asymptotiques sont également utiles en tant que spécifications formelles. La raison est que celles-ci permettent de raisonner de façon modulaire à propos du coût d'un programme : une borne en O s'abstrait de l'expression exacte du coût du programme, et par là des divers détails d'implantation. Par ailleurs, nous illustrons, à l'aide d'exemples simples, un certain nombre de difficultés liées à l'utilisation rigoureuse de la notation O, et qu'il est facile de négliger lors d'un raisonnement informel.Ces considérations sont mises en pratique en formalisant d'une part la notation O dans l'assistant de preuve Coq, et d'autre part en étendant CFML, un outil existant dédié à la vérification de programmes, afin de permettre à l'utilisateur d'élaborer des démonstrations robustes et modulaires établissant des bornes de complexité asymptotiques. Nous étendons la logique de séparation avec crédits temps¿qui permet de raisonner à la fois sur des propriétés de correction et de complexité en temps¿avec la notion de crédits temps négatifs. Ces derniers augmentent l'expressivité de la logique, donnent accès à des principes de raisonnement commodes et permettent d'exprimer certaines spécifications de manière plus élégante. Au niveau des spécifications, nous montrons comment des bornes de complexité asymptotique avec O s'expriment en logique de séparation avec crédits temps. Afin d'être capable d'établir de telles spécifications, nous développons une méthodologie qui permet à l'utilisateur de développer des démonstrations qui soient à la fois robustes et menées à un niveau d'abstraction satisfaisant. Celle-ci s'appuie sur deux principes clefs : d'une part, un mécanisme permettant de collecter et remettre à plus tard certaines contraintes durant une démonstration interactive, et par ailleurs, un mécanisme permettant de synthétiser semi-automatiquement une expression de coût, et ce sans perte de généralité.Nous démontrons l'utilité et l'efficacité de notre approche en nous attaquant à un certain nombre d'études de cas. Celles-ci comprennent des algorithmes dont l'analyse de complexité est relativement simple (par exemple, une recherche dichotomique, déjà hors de portée de la plupart des approches automatisées) et des structures de données (comme les "binary random access lists" d'Okasaki). Dans notre étude de cas la plus significative, nous établissons la correction et la complexité asymptotique d'un algorithme incrémental de détection de cycles publié récemment. Nous démontrons ainsi que notre méthodologie passe à l'échelle, permet de traiter des algorithmes complexes, donc l'analyse de complexité s'appuie sur des invariants fonctionnels subtils, et peut vérifier du code qu'il est au final possible d'utiliser au sein de programmes réellement utiles et utilisés.