From: Julien Signoles <Julien.Signoles@cea.fr>
To: Frama-C public discussion <frama-c-discuss@lists.gforge.inria.fr>,
caml list <caml-list@inria.fr>,
gdr.gpl@imag.fr
Subject: [Caml-list] Frama-C related postdoc positions at CEA LIST
Date: Tue, 10 Feb 2015 11:11:39 +0100 [thread overview]
Message-ID: <54D9D95B.3090009@cea.fr> (raw)
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
reply other threads:[~2015-02-10 10:11 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=54D9D95B.3090009@cea.fr \
--to=julien.signoles@cea.fr \
--cc=caml-list@inria.fr \
--cc=frama-c-discuss@lists.gforge.inria.fr \
--cc=gdr.gpl@imag.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