On sait décider (assez efficacement) la satisfiabilité de formules logiques portant sur l’arithmétique entière (linéaire), réelle, ou encore sur des entiers binaires de taille fixée. Ceci est très utile pour l’analyse automatique de programmes (recherche automatique de bugs, abstraction par prédicats...), où l’on exprime les traces d’exécution de programme ayant certaines propriétés (p.ex. mener à un bug) comme des solutions de telles formules.
Malheureusement, certaines classes de formules, par ailleurs très faciles à construire et qui arrivent naturellement dans certains problèmes d’analyse de programmes, font exploser la complexité des procédures de décision usuelles. Cependant, il est souvent possible de réarranger ces formules par ajout de contraintes « superflues » mais qui accélèrent grandement le calcul.
L’objet du stage est d’étudier un mécanisme automatique pour faire cela, au moins pour certains types courants de formules.
Compétences demandées :
- notions de logique mathématique
- programmation en Objective Caml ou C++
Travail attendu :
- conception de méthodes d’optimisation de formules SMT
- implantation dans un outil
Ce sujet pourra se poursuivre en thèse. Contacter : David Monniaux, laboratoire VERIMAG <David.Monniaux>
