Méthodes de raisonnement quantitative pour les logiques probabilistiques – QuaReMe

Le but de ce projet est de faire progresser les techniques pour prouver formellement l'exactitude des programmes qui utilisent des opérations probabilistes telles que, par exemple, la génération de nombres aléatoires. Il est important de noter que nos techniques seront quantitatives, exprimant les propriétés numériques des programmes plutôt que, comme cela est plus courant en logique, les propriétés booléennes (vrai, faux). Cela permettra d'utiliser plusieurs idées familières issues de l'analyse, telles que l'approximation et la convergence, dans le contexte de la vérification formelle. Notre but est d'exploiter ces idées pour: (A) résoudre des problèmes ouverts de longue date dans le domaine qui n'ont pas été explorés jusqu'à présent principalement que en utilisant des méthodes classiques basées sur la sémantique booléenne, (B) concevoir de nouveaux systèmes de preuve pour mieux prouver les propriétés quantitatives des programmes et (C) implémenter ces systèmes de preuve en utilisant l'assistant de preuve Coq, permettant des applications pratiques de notre travail.