From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id EE3FF7F6CB for ; Tue, 10 Feb 2015 11:11:37 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of Julien.Signoles@cea.fr) identity=pra; client-ip=132.168.224.8; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="Julien.Signoles@cea.fr"; x-sender="Julien.Signoles@cea.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of Julien.Signoles@cea.fr) identity=mailfrom; client-ip=132.168.224.8; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="Julien.Signoles@cea.fr"; x-sender="Julien.Signoles@cea.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@oxalide-out.extra.cea.fr) identity=helo; client-ip=132.168.224.8; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="Julien.Signoles@cea.fr"; x-sender="postmaster@oxalide-out.extra.cea.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BJAQDT2NlUnAjgqIRCGoNYWsMXhw9DAQEBAQEBEAEBAQEBBg0JCRQuhBE6GyU9FhgDAgECAUsBDAYCAQGIKQ03zUoMARsEjxURAYUBBZJxjB6MNYQRbgEBgQmBNwEBAQ X-IPAS-Result: A0BJAQDT2NlUnAjgqIRCGoNYWsMXhw9DAQEBAQEBEAEBAQEBBg0JCRQuhBE6GyU9FhgDAgECAUsBDAYCAQGIKQ03zUoMARsEjxURAYUBBZJxjB6MNYQRbgEBgQmBNwEBAQ X-IronPort-AV: E=Sophos;i="5.09,549,1418079600"; d="scan'208";a="121076283" Received: from oxalide-out.extra.cea.fr ([132.168.224.8]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 10 Feb 2015 11:11:37 +0100 Received: from pisaure.intra.cea.fr (pisaure.intra.cea.fr [132.166.88.21]) by oxalide.extra.cea.fr (8.14.2/8.14.2/CEAnet-Internet-out-2.3) with ESMTP id t1AABbdE018901; Tue, 10 Feb 2015 11:11:37 +0100 Received: from pisaure.intra.cea.fr (localhost [127.0.0.1]) by localhost (Postfix) with SMTP id 0225D2059B9; Tue, 10 Feb 2015 11:12:28 +0100 (CET) Received: from muguet2.intra.cea.fr (muguet2.intra.cea.fr [132.166.192.7]) by pisaure.intra.cea.fr (Postfix) with ESMTP id E74B62058D9; Tue, 10 Feb 2015 11:12:27 +0100 (CET) Received: from [10.8.33.83] (is006613.intra.cea.fr [10.8.33.83]) by muguet2.intra.cea.fr (8.13.8/8.13.8/CEAnet-Intranet-out-1.2) with ESMTP id t1AABaJ9030516; Tue, 10 Feb 2015 11:11:36 +0100 Message-ID: <54D9D95B.3090009@cea.fr> Date: Tue, 10 Feb 2015 11:11:39 +0100 From: Julien Signoles Organization: CEA LIST User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130329 Thunderbird/17.0.5 MIME-Version: 1.0 To: Frama-C public discussion , caml list , gdr.gpl@imag.fr Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Validation-by: julien.signoles@cea.fr Subject: [Caml-list] Frama-C related postdoc positions at CEA LIST Hello, The CEA LIST, Software Security Labs (LSL) is looking for candidates for 2 postdoc positions to begin as soon as possible at Saclay, France. * Quick position descriptions: Both positions include theoretical research and OCaml development related to Frama-C, a framework for code analysis of C programs. 1. Function Synthesis for C Programs from Formal Specifications: the aim of this postdoc is to automatically generate a function body that satisfies a given function contract. This way, it becomes possible to test a function which calls an undefined-but-specified function. See link below for details. 2. Program Transformation for Information Flow Analysis of C Programs: the aim of this 18-months research-engineer position is to improve a program transformation tool which tracks information flows of C programs. See link below for details. * Context: The successful candidates will work in the CEA LIST's new offices located at the heart of Campus Paris Saclay, in the largest European cluster of public and private research. * Requirements: Candidates should have a Ph.D. in Computer Science (at least, the defense is planned soon). They should be familiar with several of the following topics: - functional programming (OCaml) - semantics of programming languages (ISO C 99) - compilation techniques - formal specification - logic (first subject) - information flow security (second subject) * Application: Applicants should send an email to Julien Signoles (Julien.Signoles _at_ cea.fr) including a CV and a motivation letter. * Links: 1. https://bts.frama-c.com/dokuwiki/lib/exe/fetch.php?media=mantis:frama-c:postdoc:sujet_postdoc_generation_from_spec.pdf 2. https://bts.frama-c.com/dokuwiki/lib/exe/fetch.php?media=mantis:frama-c:postdoc:sujet_cdd_information_flow.pdf Best regards, Julien Signoles -- Researcher-engineer CEA LIST, Software Security Labs tel:(+33)1.69.08.00.18 fax:(+33)1.69.08.83.95 Julien.Signoles@cea.fr