Vérification formelle, Structures de données concurrentes, Linéarisabilité, Model Checking, Réduction d'ordre partielle, Protocoles de consensus, Raffinement

Les services automatisés modernes reposent sur des logiciels concurrents où plusieurs demandes sont traitées par différents processus en même temps. Ces processus s'exécutent simultanément sur une seule machine ou dans un système distribué avec plusieurs machines reliés par un réseau. Les demandes concernent généralement le traitement de données stockées dans des structures de données qui fournissent des implémentations de types de données abstraits (ADT) courants tels que des files d'attente, des tables clé-valeur et des ensembles. Les structures de données elles-mêmes sont concurrentes dans le sens où elles permettent des opérations qui peuvent s'exécuter simultanément. Développer de telles structures de données concurrentes ou même les comprendre et raisonner dessus peut être difficile. Cela vient du fait que la synchronisation entre les opérations de ces structures de données doit être minimisée pour réduire le temps de réponse et augmenter le débit, mais cette synchronisation doit également être adéquate pour assurer la conformité à leur spécification. Ces contraintes qui s'opposent, ainsi que le défi général du raisonnement sur les entrelacements entre les opérations, font des structures de données concurrentes une source d'erreurs de programmation insidieuses, difficiles à reproduire, localiser ou corriger. Par conséquent, les techniques de vérification qui peuvent vérifier la correction d'une structure de données concurrente ou (si elle n'est pas correcte) qui peuvent détecter, identifier et corriger les erreurs qu'elle contient, sont très importantes. Dans cette thèse, nous introduisons de nouvelles approches algorithmiques pour améliorer la fiabilité des structures de données concurrentes. Pour les structures de données à mémoire partagée (où les processus communiquent à l'aide d'une mémoire partagée), nous introduisons de nouveaux algorithmes pour trouver les violations de sûreté (le cas échéant) et réparer l'implémentation afin d'exclure ces violations. Pour les structures de données qui m'exécutent au-dessus d'un réseau, nous nous concentrons sur les protocoles de consensus sous-jacents et nous fournissons une nouvelle méthodologie de preuve basée sur le raffinement pour vérifier leur spécification de sûreté.