From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id C9290BC37 for ; Tue, 9 Jun 2009 10:06:55 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkkCAHu1LUqBrw8EmWdsb2JhbACYKwEBAQEBCAsKBxK0d4QKBQ X-IronPort-AV: E=Sophos;i="4.41,330,1241388000"; d="scan'208";a="41381629" Received: from ext.lri.fr ([129.175.15.4]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 09 Jun 2009 10:06:23 +0200 Received: from localhost (localhost [127.0.0.1]) by ext.lri.fr (Postfix) with ESMTP id 72258A4381; Tue, 9 Jun 2009 10:06:23 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at lri.fr Received: from ext.lri.fr ([127.0.0.1]) by localhost (ext.lri.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id iLqLCJido6lK; Tue, 9 Jun 2009 10:06:23 +0200 (CEST) Received: from [129.175.4.126] (lri4-126 [129.175.4.126]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (No client certificate requested) by ext.lri.fr (Postfix) with ESMTP id 580A7A4344; Tue, 9 Jun 2009 10:06:23 +0200 (CEST) Message-ID: <4A2E17FF.1090300@lri.fr> Date: Tue, 09 Jun 2009 10:06:23 +0200 From: Sylvain Conchon User-Agent: Thunderbird 2.0.0.17 (X11/20080925) MIME-Version: 1.0 To: caml-list@inria.fr Subject: Offre d'emploi INRIA Saclay X-Enigmail-Version: 0.95.7 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Spam: no; 0.00; lri:01 saclay:01 saclay:01 ocaml:01 ocaml:01 orsay:01 rostand:01 orsay:01 formelle:01 logiques:01 unification:01 prouveur:01 d'echecs:01 cvs:01 makefile:01 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/