[M1R 2012-2013] Analyse de programmes avec contraintes non linéaires


Laboratoire : LIAFA
Equipe : Vérification
Encadrant : Mihaela Sighireanu ( http://www.liafa.univ-paris-diderot.fr/~sighirea )

Contexte scientifique : Dans un contexte de calcul scientifique, de preuve automatique de théorèmes, ou d'analyse de programmes, on a parfois besoin de montrer qu'un système d'inégalités non linéaires n'a pas de solutions ou de calculer une approximation de ses solutions.
Nous avons développé une technique et une représentation symbolique de telles contraintes qui permet d'obtenir une réponse exacte ou approchée pour ce problème. D'autres chercheurs ont proposé des techniques basés sur l'utilisation d'outils de calcul scientifique (Mathematica, par exemple) ou la programmation semi-linéaire.

Sujet : Il n'est pas clair comment ces différents travaux se comparent quant il s'agit de résoudre des systèmes non-linéaires provenant de l'analyse de programmes avec données numériques. Le stagiaire doit mettre en place une telle comparaison, premièrement théorique et puis pratique de ces techniques.

Connaissances préalables souhaitées :