2020-03141 - Ingénieur/e scientifique contractuel : vérification formelle et dynamique (SMT)
The offer description below is in French

Contract type : Fixed-term contract

Renewable contract : Oui

Level of qualifications required : PhD or equivalent

Fonction : Temporary scientific engineer

Level of experience : From 3 to 5 years

About the research centre or Inria department

Le centre Inria Rennes - Bretagne Atlantique est un des huit centres d’Inria et compte plus d'une trentaine d’équipes de recherche. Le centre Inria est un acteur majeur et reconnu dans le domaine des sciences numériques. Il est au cœur d'un riche écosystème de R&D et d’innovation : PME fortement innovantes, grands groupes industriels, pôles de compétitivité, acteurs de la recherche et de l’enseignement supérieur, laboratoires d'excellence, institut de recherche technologique.

Context

Inria, l’institut national de recherche dédié aux sciences du numérique, promeut l'excellence scientifique et le transfert pour avoir le plus grand impact. Il emploie 2400 personnes. Ses 200 équipes-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3000 scientifiques pour relever les défis des sciences informatiques et mathématiques, souvent à l’interface d’autres disciplines. Inria travaille avec de nombreuses entreprises et a accompagné la création de plus de 160 start-ups. L'institut s’efforce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l’économie.

 

Assignment

Plateforme Padrone est un projet de création d’entreprise issue de l’équipe de recherche PACAP du centre de Rennes. L’objectif de Plateforme Padrone est de développer et commercialiser une suite logicielle améliorant les fonctionnalités d’analyse basées sur la trace d’exécution d’un programme. Les technologies utilisées dans le cadre du projet de création d’entreprise sont : PADRONE (https://team.inria.fr/pacap/software/padrone/) et des algorithmes intégrés en cours de développement.

Plateforme Padrone est à la recherche d’un ingénieur de recherche avec des compétences en vérification formelle et dynamique, et en applications diverses du SMT (« Satisfaction Modulo Théories ») pour finaliser le premier volet technique du projet qui mènera à un prototype fonctionnel à tester en environnement réel.

Cette mission de 6 mois devrait naturellement être reconduite si les premiers résultats sont conclants.

Main activities

L’objectif de la mission sera de :

  • La vérification formelle des algorithmes par SMT ou assistante de preuve,
  • La vérification du modèle d’automate représentatif du traitement du flux de trace
  • La vérification partielle et légère de façon dynamique lors de l’exécution
  • Les essais automatisés de façon classique et/ou concolique.

Ensuite, nous avancerons sur l’amélioration de la plateforme par des fonctionnalités nouvelles basées sur l’analyse de chemins et des modèles sémantiques de bas niveau :

  • Découverte des chemins prises par des valeurs d’intérêt dans la mémoire et dans les registres d’exécution, pour exposition par API et par représentation visuelle
  • Déduction des plages de valeur possibles aux points d’intérêt dans la trace, pour exposition par API et par représentation visuelle
  • Analyse concolique pour faciliter une API qui propose des transformations de trace, tout en préservant la sémantique à gros grain, y compris :
    • réduction ou augmentation des itérations des cycles
    • transformation du binaire par des instructions équivalentes ou compatibles

 Plusieurs autres fonctionnalités avancées seront développées  à la sortie du premier produit.

 

Skills

Compétences techniques et niveau requis :

  • Compétences multiplies et approfondies en vérification :
    • preuve certifiée d’algorithme par assistant de preuve, et/ou
    • vérification du modèle d’automate par SMT, et/ou
    • vérification légère à l’exécution (surcoût bas)
  • Connaissance en analyse par raisonnement à contraintes par SMT
  • Une maîtrise des process d’essais automatisés serait un plus

Compétences relationnelles :

  • Capacité à travailler en collaboration avec des personnes d'autres domaines de compétences ;
  • Savoir évaluer et développer rapidement des solutions adaptées aux différentes problématiques client ;
  • Autonomie dans la conduite des travaux qui sont confiés ;
  • Sens du partenariat et du travail en équipe ;
  • Aisance à présenter les travaux.

Langues :

  • Excellent niveau d’anglais écrit et parlé

 

Benefits package

  • Restauration subventionnée
  • Transports publics remboursés partiellement
  • Congés: 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement)
  • Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)
  • Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
  • Accès à la formation professionnelle
  • Sécurité sociale

Remuneration

Rémunération mensuelle brute à partir de 2562 euros selon diplôme et expérience.