From: Julien Signoles <julien.signoles@gmail.com>
To: Caml List <caml-list@inria.fr>
Subject: [Caml-list] [Job] 2-year Postdoc Position on Frama-C/E-ACSL
Date: Thu, 6 Jun 2019 15:44:56 +0200 [thread overview]
Message-ID: <CAPczgCBXP32-L2FHaaVnc0yVnAN4FVFc7EG-B4AwdHHbYrak4g@mail.gmail.com> (raw)
[-- Attachment #1: Type: text/plain, Size: 1620 bytes --]
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
[-- Attachment #2: Type: text/html, Size: 2070 bytes --]
reply other threads:[~2019-06-06 13:45 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=CAPczgCBXP32-L2FHaaVnc0yVnAN4FVFc7EG-B4AwdHHbYrak4g@mail.gmail.com \
--to=julien.signoles@gmail.com \
--cc=caml-list@inria.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).