Titre : Factorisation de polynômes et satisfaisabilité d'inéquations polynomiales

Sujet proposé dans : M1 Mosig, TER --- M2 MOSIG, Projet --- M2R Informatique, Projet --- Magistere, M1 --- Magistere, M2

Responsable(s) :

Mots-clés : Polynômes multivariés, factorisation, SMT solver (Satisfaisabilité Modulo Theory), Étude expérimentale
Durée du projet : de 2 à 8 mois avec possibilité de continuer en thèse
Nombre maximal d'étudiants : 1
Places disponibles : 1
Interrogation effectuée le : 29 mars 2024, à 14 heures 03


Description

Le stage est proposée par

 
Il est supervisé par
 
Il est possible de poursuivre en thèse sur des thèmes similaires.
 
 
 
Exploitation de la factorisation de polynômes pour décider la satisfaisabilité de systèmes d'inéquations polynomiales 
 
 CONTEXTE
 
L’avionique, l’automobile, l’aérospatiale utilisent des programmes embarqués pour le pilotage automatique de leur engins.
 
Pour analyser le comportement de ces programmes et certifier leur bon fonctionnement on utilise des outils (Static Analyzer, SAT & SMT solver) qui effectuent une analyse symbolique des programmes. Ces analyses permettent de vérifier qu’un programme respecte des propriétés de sûreté telles que "La vitesse de l’engin ne dépassera jamais xxx km/h".
 
Au laboratoire VERIMAG nous développons de tels outils (en Ocaml, C, C++) et nous prouvons leur correction en COQ.
 
SUJET DU STAGE
 
Les programmes qui font des calculs de trajectoires utilisent des polynômes multi-variables, classiquement à trois variables x,y,z, tel que P(x,y,z) = x^2 + y^3 + x*z - y*z.
En particulier pour approximer des fonctions telles que sin, cos, log, tan, ...
 
Garantir la correction de tels programmes se ramènent à décider s'il existe un point (x,y,z) qui satisfait un système constitué d'équations polynomiales  P(x,y,z)=0 et d'inéquations polynomiales Q(x,y,z) >=0.
Il s'agit donc d'étudier le signe des polynômes dans l'espace (x,y,z) et pour résoudre ce problème il est avantageux de factoriser les polynômes
 
 P(x,y,z) = P1(x,y,z) * P2(x,y,z)  s'annule si P1 ou P2 s'annullent
 
 Q(x,y,z) = Q1(x,y,z) * Q2(x,y,z) est positif là où Q1 et Q2 sont positifs et là où Q1 et Q2 sont négatifs
 
L'étude se ramènent alors à celle de polynômes P1,P2,Q1,Q2 de moindre degré.
 
Des travaux précédents avec B.Grenet du LIRM ont montré qu'on pouvait efficacement extraire les facteurs affines, c'est à dire de la forme c0 + c1 x + c2 y + c3 z, des polynômes P et Q.
Or on dispose des outils pour étudier facilement le signe des polynômes comportant des facteurs affines.
 
Notre étude à révéler que les solvers SMT usuels n'exploitent pas cette information.
 
LE STAGE consiste à améliorer la résolution des solveurs SMT en exploitant la factorization et la règle des signes ( plus * plus = plus, moins * moins = plus, ...).
 
MOTS-CLEFS
 
Polynômes multivariés, factorisation, SMT solver (Satisfaisabilité Modulo Theory), Étude expérimentale
 
 
PRÉ REQUIS
 
Le candidat/la candidate devra
 - être à l'aise avec les notions mathématiques de polynômes et de facteurs (univariables),
 - être à l'aise avec les raisonnements logiques,
 - savoir programmer en python,
 - avoir envie d'apprendre à utiliser un solver SMT et un logiciel de mathématique (Sage, Mathematica),
 - être intéressé par la preuve automatique
 
 
RÉFÉRENCES BIBLIOGRAPHIQUES
 
- Tung, V.X., Van Khanh, T. and Ogawa, M., "raSAT: An SMT Solver for Polynomial Constraints", Automated Reasoning: 8th International Joint Conference on Automated Reasoning (IJCAR), 2016.
available at url :  https://www.jaist.ac.jp/~s1310007/papers/IJCAR_2016_raSAT%20an%20SMT%20Solver%20for%20Polynomial%20Constraints.pdf
 
 
- Passmore, G. O., Paulson, L. C., & de Moura, L. M. (2012). Real Algebraic Strategies for MetiTarski Proofs. AISC/MKM/Calculemus, 7362, 358-370.
available at url : https://www.cl.cam.ac.uk/~lp15/papers/Arith/cicm2012.pdf