Le LIPN recrute un· maître·sse de conférences en vérification formelle

PROFIL : MCF 27 – Institut Galilée – LIPN
Profil court : Informatique
Profil : Vérification formelle

Enseignement :

Le Département d’Informatique de l’Institut Galilée intervient dans diverses formations de l’Institut Galilée : licences, masters, EUR, classes préparatoires, école d’ingénieurs Sup-Galilée. La personne recrutée sera rattachée au département d’Informatique de l’Institut Galilée. Elle interviendra dans différents champs de l’informatique de tous niveaux et parcours des formations assurées par le département, et notamment, dans les enseignements des domaines de base.

Le département a de nombreux besoins, notamment en génie logiciel, en bases de données avancées, en administration systèmes et en programmation orientée objet. La disponibilité à intervenir dans un de ces domaines sera appréciée. Il sera possible d’intervenir en Master sur des enseignements en lien avec le domaine de la spécification et la vérification formelles. Il est attendu que la personne recrutée soit volontaire pour s’impliquer dans la gestion du département en prenant des responsabilités pédagogiques telles que la responsabilité de cours et/ou d’année et/ou l’accompagnement des étudiants.

Dans le cadre de la loi « Orientation et Réussite des Étudiants (ORE) » des moyens financiers ont été obtenus notamment dans le cadre de l’augmentation des capacités d’accueil. Les enseignements seront effectués en licence et prioritairement en première année de licence.

Département ou filière d’enseignement : Informatique – Institut Galilée

Lieu(x) d’exercice : Campus de Villetaneuse – Université Sorbonne Paris Nord

Contact :

Président du département d’informatique : Kaïs Klai
departement.informatique.galilee@univ-paris13.fr
www-galilee.univ-paris13.fr

Recherche :

Le Laboratoire d’Informatique de Paris-Nord (LIPN – CNRS UMR 7030) souhaite renforcer l’axe Vérification de l’équipe LoVe par le recrutement d’un.e Maître de Conférences.

Les travaux de recherche de l’axe Vérification s’articulent autour de la vérification formelle de modèles pour la sûreté et la sécurité des systèmes. Les modèles formels considérés sont variés (réseaux de Petri, automates temporisés, automates paramétrés, automates à piles, …) tout comme les logiques exprimant leurs propriétés (LTL, CTL, TCTL, ATL, …) prenant ainsi en compte sous plusieurs perspectives les systèmes étudiés. La diversité de ces modèles pose des défis théoriques et pratiques rendant la vérification formelle plus complexe (pouvoir d’analyse inversement proportionnel au pouvoir d’expression). Les travaux de l’équipe visent à repousser les limites du model checking en proposant des approches de réduction de l’espace d’états différentes et complémentaires (structures symboliques, modularité, ordre partiel, parallélisation, ).

L’adaptation et l’application des approches proposées à des domaines particuliers (algorithmes distribués, protocoles réseaux, détection de virus, sécurité, processus métiers, gestion des ressources dans le cloud, diagnostic,) constituent également un objectif important. La prise en compte des spécificités de ces domaines permet de concevoir des approches de vérification ciblées et efficaces par rapport à une approche de vérification généraliste. La complémentarité des compétences de l’équipe est un atout majeur pour répondre à ces défis.

Les approches développées sont mises en œuvre au travers de différents outils (IMITATOR, SMODIC, STAMAD, CosyVerif, Helena, PMCSOG) qui permettent d’évaluer la pertinence des résultats obtenus sur des études de cas et d’accroître la visibilité de l’équipe sur la scène internationale.

L’expertise de la personne recrutée et son projet de recherche doivent s’intégrer dans les travaux de l’équipe. Il est attendu que la personne recrutée soit désireuse de travailler en équipe sur des problématiques scientifiques à court et long termes.

Lieu(x) d’exercice : Campus de Villetaneuse

Laboratoire d’accueil : Laboratoire d’Informatique de Paris Nord (LIPN) – CNRS UMR 7030

Contact :

Directrice du LIPN : Frédérique Bassino
frederique.bassino@lipn.univ-paris13.fr