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 80B198247D for ; Thu, 6 Jun 2019 15:45:10 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=julien.signoles@gmail.com; spf=Pass smtp.mailfrom=julien.signoles@gmail.com; spf=None smtp.helo=postmaster@mail-lf1-f41.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of julien.signoles@gmail.com) identity=pra; client-ip=209.85.167.41; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="julien.signoles@gmail.com"; x-sender="julien.signoles@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of julien.signoles@gmail.com designates 209.85.167.41 as permitted sender) identity=mailfrom; client-ip=209.85.167.41; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="julien.signoles@gmail.com"; x-sender="julien.signoles@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-lf1-f41.google.com) identity=helo; client-ip=209.85.167.41; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="julien.signoles@gmail.com"; x-sender="postmaster@mail-lf1-f41.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AIOP8gRzytWiN5nrXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?2+gVIJqq85mqBkHD//Il1AaPAdyCrasY16GI7OjJYi8p2d65qncMcZhBBVcuqP?= =?us-ascii?q?49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6?= =?us-ascii?q?JvjvGo7Vks+7y/2+94fcbglVmTaxe65+IRq5oAnet8Qbg5ZpJ7osxBfOvnZGYf?= =?us-ascii?q?ldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbD?= =?us-ascii?q?VheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLzli?= =?us-ascii?q?wJKyA2/33WisxojaJUvhShpwBkw4XJZI2ZLedycr/Bcd8fQ2dKQ8RfWDFbAo6k?= =?us-ascii?q?YIQBD+QPM+VFoYfju1QDtgGxCRW2Ce711jNEmn370Ksn2OohCwHG2wkgEsoKvn?= =?us-ascii?q?TJqNX1NbkdUeaox6fVzDXDYPVW2TD56IfWaRAqvPaBXbBtccrVyEkgCQXFgk+L?= =?us-ascii?q?qYzkMDOV0OMNs2yF4Op7Tu+vhGsnpBtwojir3Msjlo7JhocMx13C6C53zoE1Jd?= =?us-ascii?q?iiR056Z96pCJVQtzuEOIRoWM8iTXtotSAnwbMFoZ62ZDYGxIgjyhLFaPGKc5KE?= =?us-ascii?q?7g/iWeuTOzt1i29pdbSijBio60eg0PfzVsys3VZKsCVFlt7Mu2gI1xPJ68iHTu?= =?us-ascii?q?Jx/kOv2TqSzgzT5O5JLV0umarULJ4hxbEwlp4NvkjZAiD2n0D2gLeXdkUi5Oeo?= =?us-ascii?q?9/zqbqv6qpKYLYN5iQHzPr4zlsG+A+k0KAcDU3WD9eS5zrLj/En5QLtQjv0xl6?= =?us-ascii?q?nUqJLaJdkfpq64HQBV1Jwv6w2+Dzep1tQYmn0HI0xeeB+cgIjpPkvBIPH8Dful?= =?us-ascii?q?n1uslzJry+jcPrL9GpXNMmTDkLD5cLlh8UFczQ4zwclb55JVEbEBPOn+WlTxtd?= =?us-ascii?q?zdFh82KRa4w+fhCNVn14MRQ3iDAqGDMPCajVjdzesqJ6GoZZQJ8GL2Iv0hovrv?= =?us-ascii?q?lmMRmFkHfKDv04FBO16iGfEzAVidYHfqyuwAHmENugclBLjolVmDXDgVfHe9Wa?= =?us-ascii?q?U46yoTB4evDIOFTYeo1u/SlBynF4FbMzgVQmuHFm3lIsDdA69VOXCiZ/R5mzlB?= =?us-ascii?q?boCPDooo1BWgrgj/kuM1Ie/d+ylevpXmhoEsu7/j0Coq/DkxNPyzlnmXRjgtzG?= =?us-ascii?q?wNTj4ymqt4pB4lkwrR4e1Dm/VdUOdrybZJXwM9b8OOyuV7D5X2VFuEcIvQDlmh?= =?us-ascii?q?RdqiDHc6Sddjm9I=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DRBgArGPlchimnVdFlhFBCUTMohBSBH?= =?us-ascii?q?YJem0uIF4d7CQEDAQwjDAEBgUuFWhsHAQQ0EwEDAQEEAQECAQEDARMBAQEICws?= =?us-ascii?q?IKSMMgjopAYJrJR0BGxUJAxIJBzcCJAERAQUBIhODIgGBaQEDHQ+YB4MfPIsgg?= =?us-ascii?q?RQFAReCegWENAoZJw1dA4E6AgcSgSKEboZtgVc/gRGGMQOEaoI2IgSLQxuBFJw?= =?us-ascii?q?nBwKCEFoEhQtahFOIJxuDDIMQkGyUII83DyGBRYF5TSNQMYI7CYIgg1aBPokXQ?= =?us-ascii?q?DABkAIBAQ?= X-IPAS-Result: =?us-ascii?q?A0DRBgArGPlchimnVdFlhFBCUTMohBSBHYJem0uIF4d7CQE?= =?us-ascii?q?DAQwjDAEBgUuFWhsHAQQ0EwEDAQEEAQECAQEDARMBAQEICwsIKSMMgjopAYJrJ?= =?us-ascii?q?R0BGxUJAxIJBzcCJAERAQUBIhODIgGBaQEDHQ+YB4MfPIsggRQFAReCegWENAo?= =?us-ascii?q?ZJw1dA4E6AgcSgSKEboZtgVc/gRGGMQOEaoI2IgSLQxuBFJwnBwKCEFoEhQtah?= =?us-ascii?q?FOIJxuDDIMQkGyUII83DyGBRYF5TSNQMYI7CYIgg1aBPokXQDABkAIBAQ?= X-IronPort-AV: E=Sophos;i="5.63,559,1557180000"; d="scan'208,217";a="386307345" X-MGA-submission: =?us-ascii?q?MDHbdKu6OEbui+Jdvtwz2Os61LuazOtop8cp/e?= =?us-ascii?q?Ya3Rj2YuEkDwSu7qo6BKgoLllZp6s+I8O2meZOl8CqFLiVuuR544Sp3r?= =?us-ascii?q?mEhmnYHp95TDCCJ24vKyzKM0fnOiLh/3bv+k96r3uDO4RvnOz7M1CiDN?= =?us-ascii?q?Vt6CpqjkDZqTxTMO0F136Ncg=3D=3D?= Received: from mail-lf1-f41.google.com ([209.85.167.41]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 06 Jun 2019 15:45:09 +0200 Received: by mail-lf1-f41.google.com with SMTP id b11so207953lfa.5 for ; Thu, 06 Jun 2019 06:45:09 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to; bh=AOw5e/lcXAZlBVV5k69lTRRUjNlj1RUoSFoXXmwb1x4=; b=lkmUydZV3ywRmZ5f/YHfzlD3f98fEvJsfdV16U3LXIUqjBEecTlNOxtH6WByKdKXSF U8RXHlkPxAqs7NluZQU2XRYz3tZC39duLIe/6NKq2bdwcJkaz3oRKCYfCfHtdpdWY09y xabSrapC4ucWSEsCro4i/SccpZvVw9A9AYtlcHd8202jAGB9MIzaGaXK0XFlJIEOPOP+ rOjPOL7WIwdvzJ8NG5FFF/Fy8mWH/GY3APq5dgGD2ifJf//yfT0iR7DD+B1zqRDPFUtD V18rmErrfklVPPlEKi55mR9VdDeglxt93kD/kJTd8S0J1cPEyktE/Wsxdrb8t/CsRsiQ 62vA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:from:date:message-id:subject:to; bh=AOw5e/lcXAZlBVV5k69lTRRUjNlj1RUoSFoXXmwb1x4=; b=Ug2AWwxYgShXXCRxUJ1TzLGxFuMO+x97IJheQrsG8N0nHp5rAUtqRSi0vzr+9AolSP QIvIPasUJjlxIw2j88OhNx0frC7Z9dgXgvGL4qaaJhYc67+fEYFqA8waEcqcoaRfrjZQ 1W7+UCCbR4wgo+SOmaussdKXfFHiac0TF8ohEAguy3YYQXf+X+uc1nD1OVKJQjaTnvZZ XLSYKe265yzg3jbsOmv2KPuCwp+/J+Fpu6tY40cRFrjKRRIfgUbtx2PyuLWi3HXPelbT swcMx718oGtvi1GGTJO2T4vRbcgdiHVtebcoOM/I+YkgL+wk1nTDvsOEQMJBclIXS5Sy k84g== X-Gm-Message-State: APjAAAUZttqt1NR3RSRvX/OVVwp71pjKcZvVx/54iVP6SAng90l5IkAq X0ffTvpHGvJzI4xSWDsSJsZMR/TWGr0LaP6I7LV/CPRV X-Google-Smtp-Source: APXvYqz+WPLPvjZGObToyz4Je+BahwuN22gP78ViRpZAkYeKT33Z1kC1YA3z6+fB+fcu7T1cV/GY76YXxhFBtWAJPAw= X-Received: by 2002:ac2:5a4b:: with SMTP id r11mr13700361lfn.9.1559828707755; Thu, 06 Jun 2019 06:45:07 -0700 (PDT) MIME-Version: 1.0 From: Julien Signoles Date: Thu, 6 Jun 2019 15:44:56 +0200 Message-ID: To: Caml List Content-Type: multipart/alternative; boundary="000000000000094bec058aa7ecee" Subject: [Caml-list] [Job] 2-year Postdoc Position on Frama-C/E-ACSL --000000000000094bec058aa7ecee Content-Type: text/plain; charset="UTF-8" Hello, The Software Reliability and Security Lab at CEA LIST (Paris Saclay, France) is hiring a 2-year postdoctoral researcher who will improve E-ACSL, the runtime verification plug-in of Frama-C. Frama-C is an opensource framework providing several analyzers for C code. The analyzed programs can be annotated by formal specifications written in the ACSL specification language. E-ACSL is one of the existing Frama-C analyzers. It converts ACSL annotations into C code in order to verify their validity at runtime, when the program is being executed. The goal of this postdoctoral position is twofolds: on the one hand, the postdoctoral researcher shall propose new compilation schemes to support additional ACSL constructs; on the other hand (s)he shall define new compilation techniques (or adapt existing ones) in order to optimize the generated code for reducing the time overhead and the memory footprint of the generated program. The work will be guided by and evaluated on case studies providing by a few of our academic and industrial partners. Knowledge in at least one of the following fields is required: - functional programming (ideally OCaml) - C programming - compilation - static analysis - semantics of programming languages - runtime verification - formal specification A full description of the position is available online: http://julien.signoles.free.fr/positions/postdoc-eacsl.pdf Feel free to contact me for additional details, Julien Signoles -- Researcher-engineer CEA LIST, Software Reliability and Security Lab tel:(+33)1.69.08.00.18 fax:(+33)1.69.08.83.95 Julien.Signoles@cea.fr --000000000000094bec058aa7ecee Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hello,

The Software Reliability and Security Lab at CEA LIST (Paris Saclay,=20 France) is hiring a 2-year postdoctoral researcher who will improve=20 E-ACSL, the runtime verification plug-in of Frama-C.

Frama-C is an opensource framework providing several analyzers for C=20 code. The analyzed programs can be annotated by formal specifications=20 written in the ACSL specification language. E-ACSL is one of the=20 existing Frama-C analyzers. It converts ACSL annotations into C code in=20 order to verify their validity at runtime, when the program is being=20 executed.

The goal of this postdoctoral position is twofolds: on the one hand, th= e=20 postdoctoral researcher shall propose new compilation schemes to support=20 additional ACSL constructs; on the other hand (s)he shall define new=20 compilation techniques (or adapt existing ones) in order to optimize the=20 generated code for reducing the time overhead and the memory footprint=20 of the generated program. The work will be guided by and evaluated on=20 case studies providing by a few of our academic and industrial partners.

Knowledge in at least one of the following fields is required:
- functional programming (ideally OCaml)
- C programming
- compilation
- static analysis
- semantics of programming languages
- runtime verification
- formal specification

A full description of the position is available online:

=C2=A0=C2=A0=C2=A0 http://julien.sign= oles.free.fr/positions/postdoc-eacsl.pdf

Feel free to contact me for additional details,
Julien Signoles
--= =C2=A0
Researcher-engineer
CEA LIST, Software Reliability and Security Lab
tel:(+33)1.69.08.00.18 fax:(+33)1.69.08.83.95 Julien.Signoles@c= ea.fr
--000000000000094bec058aa7ecee--