--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on February 2015 ---
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 at cea.fr