Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Thèses et habilitations
Production scientifique
Habilitation à diriger des recherches de MELQUIOND Guillaume
MELQUIOND Guillaume
Habilitation à diriger des recherches
Equipe : Vérification d'Algorithmes, Langages et Systèmes

Vérification formelle pour les calculs numériques, et vice versa

Début le 01/01/1970
Direction :

Ecole doctorale : ED STIC 580
Etablissement d'inscription : vide

Lieu de déroulement :

Soutenue le 01/04/2019 devant le jury composé de :
Rapporteurs :
- Luc Jaulin (Université de Bretagne Occidentale)
- David Monniaux (CNRS)
- Warwick Tucker (Université d'Uppsala)

Autres membres du jury :
- Yves Bertot (Inria)
- Florent Hivert (Université Paris Sud)
- Claude Marché (Inria)
- Jean-Michel Muller (CNRS)
- Sylvie Putot (École Polytechnique)

Activités de recherche :

Résumé :
Mes travaux de recherche visent `a favoriser l’utilisation des outils de v ́erification formelleet en particulier les approches d ́eductives dans le domaine du calcul num ́erique. En effet,les programmes utilisent rarement l’arithm ́etique r ́eelle pour effectuer leurs calculs et ils serabattent g ́en ́eralement sur des arithm ́etiques approch ́ees telles que l’arithm ́etique `a virguleflottante, pour des raisons d’efficacit ́e. L’emploi de ces arithm ́etiques entraˆıne des erreurs decalcul qui peuvent empˆecher un programme de s’ex ́ecuter comme pr ́evu. Il est donc importantde les prendre en compte pour garantir la correction des programmes qui effectuent des calculsnum ́eriques. La subtilit ́e de l’arithm ́etique `a virgule flottante rend malheureusement l’exercicep ́erilleux, d’o`u la n ́ecessit ́e de d ́evelopper des m ́ethodes qui permettent de rendre sˆur ce travailde v ́erification.