Internships @ OCamlPro
Looking for an internship?
Stage 3-6 mois, niveau M1 à M2 (PDF)
Ce stage se concentre sur l'amélioration des performances de l'exécution symbolique de programmes WebAssembly (Wasm) dans l'outil Owi, en explorant des techniques de prédiction de branchement basées sur des algorithmes d'apprentissage automatique. L'objectif principal est de réduire les appels coûteux aux solveurs SMT en classifiant la satisfiabilité des branches. Deux approches seront examinées : une méthode d'apprentissage online, utilisant des prédictions dynamiques en temps réel, et une méthode d'apprentissage supervisé offline, basée sur un entraînement préalable à partir de formules symboliques. Les travaux incluront le développement d'une des approches, la mesure de la précision des prédictions, et l'évaluation des performances globales sur les benchmarks d'Owi. Ce projet offre l'opportunité de développer des compétences en algorithmes d'apprentissage, exécution symbolique et analyse logicielle avancée.
Stage 3-6 mois, niveau M1 à M2 (PDF)
Ce stage vise à optimiser l'exécution symbolique de programmes WebAssembly (Wasm) dans l'outil Owi, développé chez OCamlPro. L'objectif est de remplacer l'ordre d'exploration actuel, basé sur une file, par une file de priorité, et de développer des heuristiques d'exploration. Ces heuristiques permettront d'attribuer des scores aux chemins d'exécution en fonction de critères tels que le nombre d'assertions ou les caractéristiques des branches. Les résultats seront analysés à l'aide des benchmarks d'Owi. Si le temps le permet, des stratégies d'exploration alternatives comme DFS, BFS ou A* pourront être implémentées. Les candidat·e·s acquerront une expertise en OCaml, algorithmique des graphes, techniques de compilation et exécution symbolique tout en contribuant à un projet de recherche.
Stage 3-6 mois, niveau M1 à M2 (PDF)
Ce stage a pour objectif d'améliorer l'efficacité et la flexibilité de l'exécution symbolique des programmes WebAssembly (Wasm) en intégrant un support avancé pour plusieurs solveurs SMT (Satisfiability Modulo Theories). Le projet s'appuie sur l'outil de recherche Owi, développé chez OCamlPro, et exploite la bibliothèque Smt.ml pour une gestion unifiée des solveurs. L'objectif principal est de développer une passe d'analyse capable de prédire le solveur SMT optimal pour chaque programme, en se basant sur des heuristiques tirées des caractéristiques des programmes Wasm. Le stage inclut la validation des solveurs existants, l'intégration éventuelle de nouveaux solveurs, et l'évaluation des performances à travers des benchmarks. Les candidat·e·s acquerront une expertise en programmation OCaml, en exécution symbolique, en WebAssembly, et en techniques liées aux solveurs SMT, tout en contribuant à un projet de recherche.
Stage 3-6 mois, niveau M1 à M2 (PDF)
Ce stage a pour objectif de permettre à Seacoral, un orchestrateur d'outils de génération automatique de tests, d'intégrer Owi comme moteur de génération de tests ciblant des labels de couverture dans des programmes C compilés en WebAssembly. Le projet consiste à adapter l'exécution symbolique d'Owi pour interpréter les labels de couverture, optimiser son algorithme d'exploration, et produire des suites de tests exploitables. Cela inclut la gestion de données complexes (pointeurs, structures dynamiques), ainsi que la validation des modèles générés. Le stage permettra de développer des compétences avancées en OCaml, en exécution symbolique, et en génération automatique de tests tout en contribuant à un projet de recherche et industriel.
Stage 3-6 mois, niveau M1 à M2 (PDF)
Fonctionnelle et plébiscitée par la communauté OCaml, cette nouvelle version est cependant toujours en version “Beta”, et nous aimerions y apporter une gamme d'améliorations de petite et plus grande envergure. Les objectifs pourront porter sur l'amélioration de l'interface et des fonctionnalités OCaml et Web.
Stage 3-6 mois, niveau M1 à M2 Recherche (PDF)
Dans un compilateur optimisant, l'inlining est une optimisation centrale, elle permet aux autres optimisations de s'activer. Ce stage contient une large base théorique à développer, le résultat attendu pour OCamlPro sera la théorie et l'expérience acquise, et non le code lui même.
Stage 3-6 mois, niveau M1 à M3 Recherche (PDF)
OCamlPro a acquis une expertise sur le langage COBOL, et a commencé le développement de plusieurs outils, basés sur un parseur COBOL en OCaml, issu d'un travail titanesque. L'objectif de ce stage est de participer au développement de cette boîte à outils en OCaml pour COBOL .
Stage 6 mois, niveau M2 (PDF)
L'équipe compilation d'OCamlPro, qui travaille sur le compilateur OCaml, s'intéresse à spécifier formellement les définitions récursives qui ont du sens et la façon de les compiler. Le but de ce stage est de formaliser et d'implémenter un schéma de compilation plus efficace que le schéma par global store présenté dans l'article, qui est utilisé actuellement dans le compilateur.
Stage 3-6 mois, niveau M1 à M2 (PDF)
Ce stage vise à faire progresser les techniques d'exécution symbolique pour les programmes WebAssembly (Wasm), notamment à travers le développement d'optimisations dédiées au sein de l'outil Owi. Owi, un projet de recherche développé chez OCamlPro, permet une analyse précise des programmes Wasm en identifiant les valeurs d'entrée susceptibles de provoquer des erreurs, avec un support pour les programmes inter-langages et une exécution parallèle. L'objectif est d'améliorer l'efficacité de l'exécution symbolique en intégrant des passes d'optimisation spécifiques à Wasm, en s'appuyant sur des stratégies telles que la transformation en forme SSA (Static Single Assignment), l'analyse basée sur les graphes de flot de contrôle et des optimisations avancées. Les candidat·e·s acquerront une expertise en programmation OCaml, en techniques de compilation et en exécution symbolique, avec l'opportunité de contribuer à un outil de recherche.
Past internships
Stage 3-6 mois, niveau M1 à M2 Recherche (PDF)
L'objectif de ce stage est d'étudier et implémenter cette généralisation. Le stage se déroulera au sein de l'équipe flambda chez OCamlPro qui développe des optimisations sur le langage OCaml.
Stage 3-6 mois, niveau M1 à M2 (PDF)
[OCaml-Canvas] est une bibliothèque de canevas portable pour OCaml sur les systèmes GNU/Linux (X11 et Wayland), macOS (Quartz) et Windows (GDI), proposant également un backend Javascript pour une utilisation dans un navigateur web. Un des aspects fondamentaux de cette bibliothèque est de limiter au strict minimum les dépendances à des bibliothèques externes, afin de maximiser la portabilité.
Stage 6 mois, niveau M2 Recherche (PDF)
L'objectif est d'étudier la faisabilité de cette analyse, y compris documenter les choix possibles et leurs avantages et désavantages respectifs. Le stage se déroulera au sein de l'équipe flambda qui développe des optimisations sur le langage OCaml. Le travail réalisé a vocation à être intégré au compilateur officiel par l'équipe flambda par la suite.
Stage 3-6 mois, niveau M1 à M2 Recherche (PDF)
Le but premier de ce stage sera de compiler Alt-Ergo sous windows grâce aux outils de la communauté comme la cross compilation de Dune ou opam-cross-windows. Le second but de ce stage sera de mettre en place une intégration continue de cette compilation sous windows sur le dépot Github d'Alt-Ergo via des services comme Azure de Microsoft.
Stage 3-6 mois, niveau M1 à M2 Recherche (PDF)
Le premier but de ce stage serait de faire un état des lieux des travaux effectués sur le fuzzing des outils supportant le standard smt-lib, ainsi qu'étudier les résultats de tels outils de fuzzing sur Alt-Ergo. Dans un second temps, le but sera de créer un fuzzer pour le langage d'entrée d'Alt-Ergo.
Stage 3-6 mois, niveau M1 à M2 (PDF)
La première tâche du stage serait de renforcer la mise en place et l'intégration de l'outil benchpress de Simon Cruanes sur notre serveur. La seconde tâche concernera l'automatisation de tests. Pour cela nous souhaiterions mettre en place un système qui teste notre branche principale du dépôt Github d'Alt-Ergo dès que cette dernière est modifiée.
Stage 3-6 mois, niveau M1 à M2 (PDF)
Fonctionnelle et plébiscitée par la communauté OCaml, cette nouvelle version est cependant toujours en version “Beta”, et nous aimerions y apporter une gamme d'améliorations de petite et plus grande envergure. Les objectifs pourront porter sur l'amélioration de l'interface et des fonctionnalités OCaml et Web.
Stage 3-6 mois, niveau M1 à M2 (PDF)
De nombreux interpréteurs WebAssembly ont été développés récemment. L'idée principale de ce stage est de développer un fuzzer en OCaml pour Wasm afin de comparer les différents interpréteurs existants et s'assurer de leur cohérence.
Stage 5-6 mois, niveau M1 à M2 (PDF)
La première tâche du stage consistera à établir une liste de critères qui permet de déterminer la logique minimale d'un problème SMTLIB2, et la deuxième partie du stage sera d'implémenter ces critères dans Dolmen.
Stage 3-6 mois, niveau M1 à M2 (PDF)
Ce stage vise à intégrer le langage de spécification E-ACSL dans Owi, un outil d'exécution symbolique pour le code C compilé en WebAssembly, développé par OCamlPro. L'objectif est de permettre l'utilisation du moteur d'exécution symbolique pour analyser du code C annoté, en facilitant la génération d'assertions exécutables symboliquement. Les travaux incluront l'exploration de l'enrichissement d'E-ACSL pour tirer parti des variables symboliques et la possibilité de traduire des spécifications C en spécifications WebAssembly, potentiellement basées sur le Custom Annotations Proposal. Les stagiaires développeront des compétences en OCaml, méthodes formelles, sémantique opérationnelle et techniques de compilation.
Stage 3-6 mois, niveau M1 à M2 (PDF)
Les développeurs OCaml utilisent aujourd'hui Opam pour installer OCaml et tous les outils et bibliothèques dont ils ont besoin. Néanmoins, la documentation sur ces bibliothèques est loin d'être centralisée. L'objectif de ce stage est d'améliorer docs.ocaml.pro; de la génération de la documentation, à rendre la navigation entre les pages plus accessible et ergonomique et étendre les capacités de recherche en la rendant plus avancée.
Stage 3-6 mois, niveau M1 à M2 Recherche (PDF)
L'objectif de ce stage est de développer une interface graphique pour opam pour permettre à ses utilisateurs débutants d'accéder rapidement à ses fonctionnalités les plus avancées, tout en rendant la gestion au quotidien de multiples installations d'OCaml plus facile.