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. En revanche, quand il y a des calculs en virgule flottante, c’est plus délicat (et on ne sait guère le faire actuellement) ; il y a pourtant un intérêt pratique et industriel certain à cela (analyse automatique de programmes, recherche automatique de bugs..).
L’objet du stage est d’étudier des méthodes de décision sur les flottants (l’encadrant de stage a des idées !).
Compétences demandées :
- notions de logique mathématique
- programmation en Objective Caml ou C++
Travail attendu :
- conception de méthodes de décision de formules SMT avec flottants
- implantation dans un outil
Ce sujet pourra se poursuivre en thèse. Contacter : David Monniaux, laboratoire VERIMAG <David.Monniaux>
