Description
Date depot: 14 octobre 2020
Titre: Exploitation des symétries locales pour la résolution des problèmes SAT.
Directeur de thèse:
Souheib BAARIR (LRE)
Encadrant :
Claude DUTHEILLET (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Avec l’intégration toujours plus grande, des systèmes informatiques dans des applications
critiques (métro, voitures, centrales-nucléaires, blocs opératoires, etc), assurer la correction des
programmes devient une nécessité. Si l’utilisation systématique de tests permet d’améliorer
grandement la qualité du code, elle ne peut réellement garantir leur correction.
A l’inverse, les techniques dites de model-checking, qui vérifient la validité du workflow
applicatif (modélisé par un graphe d’états) par rapport à une propriété donnée, permettent
de garantir la correction des programmes. Ces techniques reposent, essentiellement, sur deux
théories : celle basée sur les automates et celle fondée sur la satisfiabilité booléenne (SAT). Dans
les deux théories l’ennemi commun est le problème bien connu de l’explosion combinatoire. En
utilisant les automates, le problème se manifeste par une consommation mémoire démesurée,
alors qu’en utilisant le SAT, le problème se manifeste sous la forme d’un temps de calcul
extrêmement long.
Cependant, certains systèmes exhibent des comportements symétriques, i.e., les composants
du système se comportent de façon identique à une permutation des identités près. Ces
symétries se traduisent naturellement sur les problèmes SAT générés lors de la vérification :
en effet, les permutations détectées au niveau du système se traduisent (de façon triviale) par
des permutations, dont l’application laisse la formule SAT invariante. Ainsi, la prise en compte
de symétries lors la résolution du problème est censée réduire considérablement le temps de
calcul !
Doctorant.e: Saouli Sabrine