Offre d'emploi INRIA Saclay

[Sylvain Conchon <sylvain.conchon@lri.fr>]

Offre d'emploi: Ingénieur de développement


Dans le cadre d'une action de développement technologique (ADT), le
centre de recherche INRIA Saclay souhaite recruter un programmeur
OCaml en tant qu'ingénieur de développement pour une durée d'un an
(renouvelable une fois) à partir de l'automne 2009.

Mots clés: vérification de programmes, démonstration automatique, OCaml


Lieu de travail:
----------------

Centre de recherche INRIA Saclay - Ile de France
Parc Orsay Université
ZAC des vignes
32, rue Jean Rostand - Bât K
91893 Orsay Cedex France  Cedex


Contexte:
---------

L'équipe de recherche ProVal propose des méthodes et outils de
développement logiciel faisant une large place à la preuve de
programmes assistée par ordinateurs. Des applications logicielles
critiques dans les domaines du transport, des transactions bancaires
ou des télécommunications sont mises rapidement sur le marché. Pour
garantir aux utilisateurs un comportement acceptable, il est
nécessaire qu'une large part de vérification soit réalisée de manière
mécanique. Nous développons des environnements qui à partir d'une
description formelle du comportement attendu du programme, exprimée
par le développeur dans un langage adapté à son problème, engendre des
formules logiques (obligations de preuve) suffisantes pour garantir la
correction du programme. Ces formules peuvent ensuite être traitées
par des démonstrateurs adaptés tel que Alt-ergo[1].

Ces activités de l'équipe se déroulent dans le cadre de contrats ANR
Decert (Déduction certifiée) et U3CAT (Unification de techniques
d'analyse statique de codes C critiques). Ce dernier associant en
particulier les partenaires industriels Airbus France et Dassault
aviation.



Activité:
---------

L'ingénieur réalisera des outils et des expérimentations scientifiques
autour du démonstrateur Alt-Ergo afin d'améliorer son efficacité dans
le domaine de la certification de codes critiques.

 * Améliorations des performances d'Alt-Ergo comme prouveur de la
   plate-forme de certification Caveat/Frama-C/Why[2]

 * Traitement des cas d'échecs par génération de contre-exemples et
   traitement semi-interactif

 * Augmentation de la visibilité d'Alt-Ergo (e.g participation à la
   compétition internationale SMT-Comp)


Compétences:
------------

 * Formation en informatique et connaissances du développement
   logiciel et des outils associés (cvs/svn, Makefile, documentation,
   tests, débogage,...) ;

 * Langages de programmation : Ocaml;

 * Connaissances appréciées (non obligatoires): logique,
   démonstration automatique, compilation;

 * Maîtrise de l'anglais technique et scientifique;

 * Bonnes aptitudes rédactionnelles.


Contacts:
---------

Sylvain Conchon et Evelyne Contejean
{sylvain.conchon, evelyne.contejean}@lri.fr


[1] http://alt-ergo.lri.fr
[2] http://frama-c.cea.fr/