Analyse statique des algorithmes distribués tolérants aux pannes – SAFTA

Les structures de données distribuées tolérantes aux pannes sont
extrêmement complexes en raison des multiples sources de
non-déterminisme.
Le projet envisage d'augmenter la confiance que nous avons dans les implantions distribuées tolérantes aux pannes. Nous étudierons les abstractions partiellement synchrones, qui réduisent le nombre d'entrelacements en simplifiant les différents types de raisonnement et les arguments de preuve.
Nous allons utiliser la synchronie partielle pour prouver des théorèmes de réduction de la sémantique asynchrone vers une sémantique partiellement synchrone, qui permettront l'extension de preuves du monde synchrone vers le monde asynchrone.
Nous envisageons aussi de définir un langage de programmation spécifique à ce domaine, qui permettra aux programmeurs de se concentrer sur la tâche algorithmiques, qui sera compilé vers du code asynchrone, et qui sera équipé d’un moteur de vérification automatique.