POSTDOC WP5.3

Fiche de poste : post-doctorant, Lieu : Université Paris-Est Créteil, Laboratoire LACL. Durée : 12 mois. Cadre : ANR MARMOTE

Contexte: le projet MARMOTE (https://wiki.inria.fr/MARMOTE/Accueil) a pour objectif de réaliser le prototype d'un environnement logiciel dédié à la modélisation avec les chaînes de Markov. Il regroupe sept équipes partenaires expertes en analyse markovienne, qui développent des algorithmes de résolution avancés et des applications dans différents domaines scientifiques: fiabilité, systèmes distribués, vérification, biologie, chimie, physique et économie.

Le ou la candidat(e) devra maitriser les techniques de modélisation stochastiques et de méthodes formelles. Il ou elle devra avoir obtenu un doctorat en informatique ou en mathématiques appliquées avec dans ce cas de très bonnes connaissance en informatique. Le poste est associé essentiellement au WP 5.3 portant sur la stochastique vérification par simulation. Le candidat devra travailler avec l'équipe Spécification et Vérification de Systèmes au laboratoire LACL et il devra interagir avec des équipes du projet ANR MARMOTE, à Versailles, Grenoble, Montpellier, et Paris. Les logiques temporelles comme CSL, PCTL sont définies pour les modèles markoviens et elles permettent de vérifier les probabilités de rencontrer sur les trajectoires certaines propriétés spécifiées par leurs opérateurs. Il faut explorer efficacement les trajectoires du modèle en contournant le problème d'explosion d'espace d'états et/ou l'infinité du temps (opérateur until non borné). Le candidat mettra en ouvre de nouvelles techniques de vérification qui se reposent sur les méthodes proposées par les WP 1 (Simulation Parfaite), WP2 (Simulation parallèle dans le temps), WP4 (simulation numérique). Ces méthodes seront intégrées au logiciel en collaboration avec les autres partenaires.

Diplôme : Thèse

Salaire : Selon grille ANR / UPEC

Contact : Nihal Pekergin, nihal.pekergin@u-pec.fr.