[M2R 2012-2013] Décision de formules contenant des flottants

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>