| Resumé |
Au cours des dernières décennies, les logiciels distribués ont pris une place centrale dans notre société. Ils sont utilisés dans divers domaines tels que la gestion des transactions bancaires et des achats en ligne, le télétravail, et l'enseignement à distance. Développer des logiciels distribués corrects et efficaces est un défi majeur. L'objectif de cette thèse est de proposer des techniques algorithmiques pour améliorer la fiabilité de ces logiciels, en se concentrant sur les applications logiciels qui s'exécutent au-dessus des systèmes de stockage distribués comme les bases de données ou la blockchain. Les bases de données permettent à des applications d'accéder simultanément aux données grâce à plusieurs sites répartis sur un réseau. La blockchain est un registre de stockage distribué et sécurisé par des techniques cryptographiques qui permet d'effectuer des tâches irréversibles entre différentes entités sans autorité de confiance centrale.L'exécution en parallèle d'un ensemble de transactions sur des bases de données est spécifiée à l'aide d'un formalisme appelé le modèle de cohérence. Par exemple, le modèle de sérialisabilité indique qu'un ensemble de transactions se comporte comme si elles étaient exécutées en série l'un après l'autre, même si elles se chevauchent dans le temps. Bien que simple à comprendre, la sérialisabilité entraîne une pénalité significative en terme de performance. Pour cette raison les bases de données modernes mettent en oeuvre des modèles de cohérence plus faibles. En général, il est plus complexe de mener des raisonnements sur ces modèles faibles. Dans cette thèse, nous étudions le problème de la vérification d'une propriété des applications logiciels qui s'exécutent au-dessus des bases de données appelée la robustesse. Étant donné deux modèles de cohérence comparables, une application est dite robuste si elle a le même comportement lorsqu'elle est exécutée sur deux bases de données mettant en oeuvre les deux modèles de cohérence. Dans cette thèse, nous étudions la complexité théorique de la vérification de la robustesse dans le contexte de plusieurs modèles de cohérence: causal consistency, prefix consistency, snapshot isolation, et la sérialisabilité. Nous donnons des réductions non triviales à un problème bien étudié dans la littérature de la vérification formelle, la vérification des assertions, qui permet la réutilisation des technologies de vérification existantes. Outre des résultats théoriques, nous proposons aussi des approches basées sur des sous/sur-approximations que nous évaluons sur des applications pratiques. Les applications logiciels exécutées au-dessus de la blockchain sont déployées sous la forme de smart contracts qui manipulent l'état de la blockchain. Les smart contracts sont principalement utilisés pour des opérations basées sur des crypto-monnaies valant plusieurs milliards de dollars. Par conséquent, des erreurs dans les smart contracts peuvent entraîner d'énormes pertes financières. Ces erreurs sont exacerbées par le fait que les smart contracts ne peuvent pas être modifiés une fois qu'ils sont déployés sur la blockchain. L'application des techniques de la vérification formelle pour auditer les smart contracts peut aider à éviter des erreurs coûteuses. Cependant, comme la plupart des smart contracts ne sont pas annotés avec leurs spécifications, la vérification formelle des propriétés fonctionnelles est entravée. Pour surmonter ce problème, nous explorons dans cette thèse les notions de raffinement entre smart contracts, qui permettent la réutilisationdes smart contracts vérifiés comme spécifications pour d'autres smart contracts, améliorant ainsi l'effort global de vérification |