Description
Date depot: 9 octobre 2019
Titre: Parallélisations et optimisations du Bounded Model-checking
Encadrant :
Etienne RENAULT (LRE)
Directeur de thèse:
Souheib BAARIR (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Les systèmes informatiques qui régissent notre quotidien sont omniprésents. Cela va du simple programme qui fait fonctionner un micro-onde, au logiciel, très complexe, pilotant une centrale nucléaire, en passant par nos smart-phones et nos voitures. Ainsi, garantir la fiabilité et la robustesse de ces systèmes n’est pas une option mais une nécessité absolue. L’une des approches consacrées à cet effet opère très tôt dans le processus de production d’un système informatique. Il s’agit de l’approche dite de model-checking. En effet, dès la première phase de développement, i.e., la modélisation d’une solution possible, une analyse formelle est appliquée. Cette analyse permet soit de prouver l’absence de défaillance, soit d’en exhiber une possible ce qui permet de proposer une correction. Le model-checking se décline en plusieurs techniques. Entre autres, celles basées sur la satisfiabilité (SAT) Booléenne ou d’ordre supérieur, appelées Bounded model-checking. Dans ce type d'approches, les comportements sont décrits sous la forme de problèmes SAT. La représentation mémoire est raisonnable (car utilisant des techniques symboliques), mais la difficulté est placée sur le temps de résolution (car les problèmes SAT sont des problèmes NP-complets de façon générale). Ainsi, l’aboutissement de l’analyse des systèmes informatiques étudiés est fortement conditionné par la recherche d’heuristiques et optimisations permettant de réduire le temps de calcul. Dans cette thèse, nous pensons explorer le parallélisme et les propriétés structurelles des problèmes (par exemple, les symétries, l'ordre partiel, etc.) pour l’optimisation du processus de vérification et pousser les limites des systèmes que nous pouvons analyser formellement.
Doctorant.e: Kheireddine Anissa