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 c5ff346549e7 (Postfix) with ESMTPS id 9D7205D5 for ; Thu, 15 Nov 2018 11:27:29 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.56,236,1539640800"; d="scan'208,217";a="355818070" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 15 Nov 2018 12:27:28 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 2CE53824CF; Thu, 15 Nov 2018 12:27:28 +0100 (CET) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 6404E824CF for ; Thu, 15 Nov 2018 12:27:23 +0100 (CET) Authentication-Results: mail3-smtp-sop.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-ot1-f42.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AhvpOKhCT1w1zBVtg0tA8UyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPT6psbcNUDSrc9gkEXOFd2Cra4c1KyO6+jJYi8p2d65qncMcZhBBVcuqP?= =?us-ascii?q?49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6?= =?us-ascii?q?JvjvGo7Vks+7y/2+94fcbglUhjexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfO?= =?us-ascii?q?pWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnM?= =?us-ascii?q?VhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0iS?= =?us-ascii?q?cHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRsleWSxPDI2/?= =?us-ascii?q?coUBEfYOMP1CoIXhvVYDtweyCRWuCe7p1zRGhmX23ao/0+k5FQ/GwQggH9MQv3?= =?us-ascii?q?TSsd77KaYSUe+zzKnPyTXMcehW0ir65YjKbxAhpfCMUqx2ccbL0kkvFgzFjlOX?= =?us-ascii?q?qYzhITyVzf8As2ee7+V6VOKvj3QrpB12ojiq38ohjJTCiIwSylDB7yp5wYA1KM?= =?us-ascii?q?W2SE5hf9GrDoFcty+AN4ZwX8gsQHlotT4kxrEavZO3ZisHxZQ9yxLBdvCLb5KE?= =?us-ascii?q?7x39WOuXPDx2nmhqeKiliBa36UWgyvPzVs2z0FtSqypKiNjMtnQU2xzU9siLV+?= =?us-ascii?q?Jx/kmu1DqRzQzT5eZEIUc7larfNZEt2KI/lp0WsUjbHy/2nlv5jLOOe0k65uSl?= =?us-ascii?q?7/7rb7bmq5OGKYN4lx3yPr4hl8ChGeg4NxIBX2mf+eSyzr3j+kj5Ta1Ijv0rlq?= =?us-ascii?q?nZsY7VJcIBqq6iAg9V3YAj6xG7Dzi4y9QVhnYHLFdfdxKGi4jlIU3BIPf9Dfun?= =?us-ascii?q?mVSjjC9rx+zaPr3mGpjCMmLMkLLlfbpk705cyREzzcxE6pJPCrABJerzVVXruN?= =?us-ascii?q?zZCB85KQ20zPz9BNVzzINNEV6IV4SQNaealV6T+qp7KOCJYMoRuS3hA/kj/f/n?= =?us-ascii?q?y3EjzwwzZ66siLkKbHG1GLxdIkqfZn7hmZ9VE3oOvwc4Cvfrh1uFVTNIT3m3Vq?= =?us-ascii?q?M4oDo8DdT1Xs/4WomxjenZj2+AFZpMazUDUwjUSCa6R8C/Q/4JLRmqDIpkmz0A?= =?us-ascii?q?W6KmTtZ4hx6rvQ7+jbFgK7iNo3FKhdfYzNFwotbru1Qq7zUtVpaS1miMSyd/mW?= =?us-ascii?q?ZaH2ZrjpA6mlR0zxK46YY9g/FcEoYOtfZAUwN/MoKFiuImUZb9XQXOetrPQ1Gj?= =?us-ascii?q?EI2r?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BuAABCV+1bhirSVdFiHgEGBwaBVAYLA?= =?us-ascii?q?YIoAUBPMyeDeIEdgl6QF4wTh1yHTg0jgVSGRRoHAQQzBg0BAwEBAgEBAQEBEwE?= =?us-ascii?q?BAQgLCwgpIwyCNiQBgmQlHQEbFQkDEgkHNwIkAREBBQEiE4MhAYFoAQMVD5hng?= =?us-ascii?q?x48iw2BEgUBF4J3BYQ5ChknDVqBNwIGEotzgVc/gRGGLQOEZII1IgKJBhmBAJV?= =?us-ascii?q?DBwKCGgSEG0CDK4cAGIIkgjGMII0vikkPIYETKIF3TSNQMYI7CYISGoNTgT6JF?= =?us-ascii?q?UEwAY4uAQE?= X-IPAS-Result: =?us-ascii?q?A0BuAABCV+1bhirSVdFiHgEGBwaBVAYLAYIoAUBPMyeDeIE?= =?us-ascii?q?dgl6QF4wTh1yHTg0jgVSGRRoHAQQzBg0BAwEBAgEBAQEBEwEBAQgLCwgpIwyCN?= =?us-ascii?q?iQBgmQlHQEbFQkDEgkHNwIkAREBBQEiE4MhAYFoAQMVD5hngx48iw2BEgUBF4J?= =?us-ascii?q?3BYQ5ChknDVqBNwIGEotzgVc/gRGGLQOEZII1IgKJBhmBAJVDBwKCGgSEG0CDK?= =?us-ascii?q?4cAGIIkgjGMII0vikkPIYETKIF3TSNQMYI7CYISGoNTgT6JFUEwAY4uAQE?= X-IronPort-AV: E=Sophos;i="5.56,236,1539640800"; d="scan'208,217";a="285575421" Received: from mail-ot1-f42.google.com ([209.85.210.42]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 15 Nov 2018 12:27:22 +0100 Received: by mail-ot1-f42.google.com with SMTP id n46so17712932otb.9 for ; Thu, 15 Nov 2018 03:27:22 -0800 (PST) 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=e9+X8PAJCOL2KwhpxyVwKSV6ZoF7L8tP9UmHzVVsO4A=; b=raqeW+QKQeWe14IVtFbjqmxLfIJaY8kKJVPdSCqYUOX1vI/PuBoE3AfNey2MfsKU4b BkoejtkuEwQc9icFtaCyweLIoWGVa0YAUqwmLQSzOg9mVfWiZjja/R5AOtLkfpXcVfIZ yMYnrWFHSfGV2dDgx+DFsqFlZ38BXPtOneoD+Mc8RspSutmf3MSr43ZnB9WpCFAJlU5s NILp7sf4SRfroKKZ0yU/AmGijjSw5prtRSrkXVTYuI85raxGBs0jPVwk59z13ZY1Bo63 UCp8kklUsMvP+pHWR08PxQZCaXTo2SbC2VqjCDfZIF5LKaRs6TRLaBPJsgqUyGEzEma7 zd7g== 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=e9+X8PAJCOL2KwhpxyVwKSV6ZoF7L8tP9UmHzVVsO4A=; b=EGhaURPF5IKF+02fKbyM1w/tTgillhl3nGS4RERZAyX7ANT+DwQPqSnqWxDK9SDxo0 nfNzKF0rqHn54JGk9Y5uDbzM0SBulzmY+vwI1gfLQ7cQ/yM0xBtbIrwZNHVDePcURjCd Sfq9gLDpChMO3F3rr5yx/WaLMM5gw8M/+x1CuuA1pp8dQAP7i5lKBYddxnJCbRzHCJ6G asVTkZePMoacy8+A2M0NTDa3eAOYwizzeRuRabtJtxVKnBNuYGIaVDVfSqt4FDHYiOXJ Sqlc0lptOunbBumT/THb+h+YD2zILQs8Ag3DRDQsrA/V69NqRgU+QY0htrg25hsFKC70 tPJw== X-Gm-Message-State: AGRZ1gLbdOMG4wcMg2HP0ZQhAWhE+UjUvwAeNLMYUjYPgrUJJo1BNLzk MeXaJAm4WKSMU33H54+QyoqwdRhPV1+rlyNkn/ypXDNkmzI= X-Google-Smtp-Source: AJdET5d1XEnb6+vP3GTENnrEhJQa3hI4dReGnzHdVOO6D2tRrf9kjze7PcdnUJ2TAr0xqU+vxzpCT3FiozyKSpYp5xw= X-Received: by 2002:a9d:67:: with SMTP id 94mr3556908ota.57.1542281240145; Thu, 15 Nov 2018 03:27:20 -0800 (PST) MIME-Version: 1.0 From: Julien Signoles Date: Thu, 15 Nov 2018 12:27:08 +0100 Message-ID: To: Caml List Content-Type: multipart/alternative; boundary="0000000000007672a1057ab255bc" Subject: [Caml-list] 2-year Postdoc Position on Frama-C/E-ACSL Reply-To: Julien Signoles X-Loop: caml-list@inria.fr X-Sequence: 17135 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --0000000000007672a1057ab255bc 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 to improve the Frama-C runtime verification plug-in E-ACSL. 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 adapt existing compilation techniques or define new 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: - OCaml programming (at least, functional programming) - C programming - runtime verification - compilation - static analysis - semantics of programming languages - 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 -- Caml-list mailing list. Subscription management and archives: https://sympa.inria.fr/sympa/arc/caml-list https://inbox.ocaml.org/caml-list Forum: https://discuss.ocaml.org/ Bug reports: http://caml.inria.fr/bin/caml-bugs --0000000000007672a1057ab255bc Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hello,

The Software Reliability an= d Security Lab at CEA LIST (Paris Saclay, France) is hiring a 2-year postdo= ctoral researcher to improve the Frama-C runtime verification plug-in E-ACS= L.

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

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

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

A full description of the position is avail= able online:

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

Feel free to contact me for additional detail= s,
Julien Signoles
--
Researcher-engineer
CEA LIST, Software R= eliability and Security Lab
tel:(+33)1.69.08.00.18 fax:(+33)1.69.08.83.9= 5 Julien.Signoles@cea.fr
<= /div>
--0000000000007672a1057ab255bc--