Stage - ingénieur développeur ocaml h/f

Au sein de l'organisation R&D du logiciel CATIA, vous travaillez dans l'équipe en charge du développement de l'application Stimulus.

Stimulus [1, 2] est une application de mise au point des exigences temps-réel des systèmes embarqués (automobile, aéronautique, ferroviaire, énergie, etc) qui permet de formaliser les exigences textuelles d'un système, puis de détecter, par la simulation, les exigences incorrectes, manquantes ou contradictoires.

Que veut dire simuler des exigences ? Les exigences formalisées dans Stimulus sont vues comme des contraintes sur des signaux (booléens, numériques, etc..), qui sont résolues à chaque pas d'exécution pour extraire aléatoirement une solution possible parmi l'ensemble des solutions. Une fois une valeur obtenue pour l'ensemble des signaux, l'exécution se poursuit en faisant avancer le temps. Simuler un modèle d'exigences revient ainsi à exhiber une trace d'exécution choisie aléatoirement mais compatible avec les exigences Le solveur de contraintes actuellement mis en oeuvre dans Stimulus utilise une combinaison de BDDs (Binary Decision Diagrams) [3, 4] et de polyèdres convexes, manipulés à l'aide de l'algorithme de Chernikova [5, 6]. La complexité théorique de la résolution des contraintes considérées dans Stimulus est NP-complet ou exponentielle en le nombre de variable, dans le pire des cas. La complexité en pratique sur les exemples concrets est heureusement beaucoup plus favorable. Néanmoins, notamment dans le cas des polyèdres, le pire des cas est facile à produire

Vos Missions

Objectif du stage : expérimenter d'autres solveurs de contraintes

L'objectif principal du stage est donc de remplacer la manipulation de polyèdres convexes fondée sur l'algorithme de Chernikova par un algorithme de programmation linéaire de type simplexe, implanté dans de nombreuses librairies OpenSource, pour pouvoir comparer les performances respectives des deux approches dans le cadre de Stimulus.

- Vous devrez d'abord identifier les bibliothèques de programmation linéaire existantes qui répondent aux besoins de Stimulus (arithmétique exacte, aspects incrémentaux, etc) ;
- Ensuite, vous devrez proposer une architecture adéquate pour interfacer le solveur de Stimulus avec la bibliothèque de programmation linéaire sélectionnée, et la mettre en oeuvre ;
- Enfin, il s'agira d'expérimenter la solution sur les nombreux modèles Stimulus à disposition de l'équipe.

Si le temps le permet, vous aborderez l'étape suivante consistant à expérimenter l'usage d'un solveur « SMT » (Sat Modulo Theory) comme AltErgo [7], qui remplacerait à la fois les BDDs et les polyèdres convexes. Le défi est ici d'introduire de l'aléa dans le tirage des solutions fait par un tel solveur.

Qualifications

Etudiant(e) préparant un diplôme de niveau Bac +5, Ecole d'Ingénieur ou Master Universitaire, vous vous spécialisez en Informatique et recherchez un stage de fin d'études à compter de janvier 2026.

Vous êtes familier avec le langage OCaml.

Des connaissances en analyse de programme et en méthodes formelles seront appréciées.

On attend de vous de la curiosité, de la rigueur et une certaine autonomie.

Vous serez amené(e), au cours de votre mission, à collaborer avec l'ensemble des membres de l'équipe.

Les atouts en nous rejoignant

· Environnement collaboratif et innovant

· Collaboration internationale

· Diversité des technologies, produits et solutions

· Apprentissage au sein d'une équipe experte

· Engagement en faveur de la diversité et de l'inclusion