Laboratoire: Verimag (http://www-verimag.imag.fr/)
Encadrants: Pierre Corbineau <Pierre.Corbineau@imag.fr>, David Monniaux <David.Monniaux@imag.fr>
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 borne sur ses solutions. On a même parfois besoin d’une preuve forte que cette absence de solution ou cette borne sont correctes.
Nous avons développé une technique qui produit en sortie non seulement la réponse (p.ex. "le système n’a pas d’équations") mais surtout des coefficients qui permettent une vérification facile que cette réponse est justifiée (Monniaux & Corbineau, ITP 2011).
Sujet
Notre technique souffre d’inefficacités diverses ; par exemple, elle n’exploite pas les symétries des problèmes, ou très peu. Il s’agit donc de chercher des améliorations.
Compétences Attendues
- De bonnes bases en algorithmique et recherche opérationnelle
- Connaissance souhaitable du langage Python
Contexte de Travail
Le stagiaire sera encadré par Pierre Corbineau et David Monniaux (permanents du laboratoire).
