Description
Date depot: 9 avril 2021
Titre: Vers un solveur SAT distribué efficace
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 ...), assurer la correction des
programmes devient une nécessité. Si l’utilisation systématique de tests permet d’améliorer
grandement la qualité des codes, elle ne peut réellement garantir leur correction.
À 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 validité 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 qui
peut être extrêmement long.
Or, le cloud computing rend aujourd’hui accessible une puissance de calcul autrefois réservé
aux supercalculateurs. Si les machines de ces systèmes sont toutes dotées de multicoeurs et
d’une grande capacité de mémoire, la scalabilité passe aussi par l’utilisation en parallèle d’un
grand nombre de machines. L’utilisation d’une telle architecture nécessite donc l’utilisation
d’un solveur SAT multithreadé, mais aussi distribué.