Missions

Conduire la maîtrise d'œuvre de projets sur une ou plusieurs phases du cycle de vie : analyse, conception, développement, test, intégration, déploiement dans le respect du cahier des charges, des normes et des règles de sécurité

Travailler dans un réseau d'ingénieurs en soutien de chercheurs localisés sur des sites différents

Activités

Piloter le projet sur tout ou partie de son cycle de vie
Analyser les besoins et participer à la réalisation du cahier des charges fonctionnel du projet
Assurer une veille technologique en relation avec le domaine d'application et les experts du domaine
Développement
Assurer la conception de la solution au moyen d'expertises approfondies
Définir l'architecture logicielle
Élaborer, développer et réaliser les tests
Intégration
Mettre en œuvre les activités de packaging applicatif destiné à être déployé sur un ou plusieurs sites d'exploitation
Configurer les serveurs d'intégration continue pour la compilation, les tests, le packaging et le déploiement automatique
Déploiement
Rédiger et mettre à niveau les documentations techniques et fonctionnelles
Assurer une assistance fonctionnelle et/ou technique aux exploitants et aux utilisateurs

Compétences

Connaissances
Conduite de projet et principes de génie logiciel (connaissance approfondie)
Langage de programmation fonctionnelle (de préférence OCaml, connaissance approfondie)
Programmation système (notamment parallèle/multi-thread) et réseaux IP (en C/C++)
Administration d'un système GNU/Linux
Outils de développements logiciels (utilisation collaborative de git, CI/CD, Docker, …)
Langages de script (Perl, Python)
Sécurité des systèmes d'information et de communication
Anglais niveau B2

Compétences opérationnelles
Piloter un projet (expertise)
Appliquer les techniques du domaine
Mettre en œuvre une démarche qualité (expertise)
Évaluer une solution
Savoir travailler en réseau et à distance
Assurer une veille technologique

Contexte de travail

La personne recrutée sera mutualisée entre trois laboratoires d'informatique en Île de France : IRIF (https://www.irif.fr/), LIPN (https://lipn.univ-paris13.fr/) et LMF (https://lmf.cnrs.fr/). Ses missions seront réalisées sous la responsabilité d'un IR CNRS du LIPN, chef de projets logiciels. Le lieu de travail pourra toutefois être n'importe lequel des trois laboratoires en accord avec la personne recrutée et en fonction des besoins des projets. De plus, le télétravail peut être envisagé selon la réglementation en place au CNRS.
Chaque laboratoire concerné développe des logiciels directement issus ou comme support de ses recherches. Les projets listés ci-dessous sont des exemples de projets dont la personne recrutée pourra être en charge et des missions y associés :

CDuce (https://www.cduce.org/) : CDuce est un langage fonctionnel avec polymorphisme et surcharge. Les missions incluent la consolidation des fonctionnalités nouvelles issues de la recherche (enregistrement, raffinement de types, …) ainsi que des tâches de maintenance (maintien de la compatibilité avec OCaml, release, …).

Usuba (https://usubalang.github.io/usuba/) : Usuba est un langage de programmation dédié à la cryptographie symétrique haute-performance. Son compilateur est implémenté en OCaml. Les missions incluent le déploiement d'un système d'intégration continue et des refactorisations de code.

Cubicle (https://cubicle.lri.fr/) : Cubicle est un model-checker permettant de vérifier des propriétés de sûreté de systèmes manipulant des tableaux. Les missions incluent le portage à OCaml 5.0 Multicore, l'interface graphique, la compilation sous Windows.

SPEN (https://www.irif.fr/~sighirea/spen/) : SPEN est un solveur pour la logique de séparation. Il est utilisé pour la vérification de programmes avec un tas mutable (C, Java, etc). Il est développé en C et en OCaml. SPEN participe à la compétition des solveurs pour la logique de séparation, SL-COMP. Les missions incluent la mise à jour du code sur les plateformes de la compétition SL-COMP, l'intégration du parseur de la compétition et du typeur OCaml pour SMTLIB2.

IMITATOR (https://www.imitator.fr/) : Model checker pour la vérification de systèmes temporisés paramétrés. Il est codé en OCaml. Les missions incluent une extension de la syntaxe, et une amélioration du système multi-cœur avec les nouvelles fonctionnalités apportées par Ocaml 5.

PMC-SOG (https://lipn.univ-paris13.fr/pmc-sog/) : Model checker parallèle pour la vérification de systèmes concurrents en utilisant le graphe d'observation symbolique. Il est codé en C++ et utilise le mécanisme des threads fourni par C++20. Les missions incluent la parallèlisation de tests de vacuité et l'implémentation de la réduction basée sur les ordres partiels.