>
> The CEA LIST, Software Security Lab (LSL) is looking for candidates for
> several postdoc positions in the area of software verification, to begin
> as soon as possible at Paris-Saclay, France. More details on:
> http://sebastien.bardin.free.fr/2015-postdoc-positions.html
>
>
> * Host Institution
>
> Within CEA LIST, LSL is a twenty-person team dedicated to software
> verification, with a strong focus on real-world applicability and
> industrial transfer. We design methods and tools that leverage
> innovative approaches to ensure that real-world systems can comply with
> the highest safety and security standards. CEA LIST's new offices are
> located at the heart of Campus Paris Saclay, in the largest European
> cluster of public and private research.
>
>
> * Quick position descriptions:
>
> All positions include theoretical research as well as prototyping
> (preferably in OCaml).
>
>
> 1. constraint solving and decision procedures (with François Bobot):
> The aim of the SOPRANO project http://soprano-project.fr/ is to
> prepare the next generation of verification-oriented solvers, by
> combining principles from both Satisfiability Modulo Theory and
> Constraint Programming. Within this ambitious agenda, the successful
> candidate will investigate one of the following topics:
> . model synthesis for quantified 1st-order logic formulas, with
> applications to counter-example generation and test generation;
> . efficient satisfiability solving for still-challenging theories, such
> as bitvector theory and floating-point arithmetic theory
>
>
> 2. Source-level software verification and testing (with Nikolai
> Kosmatov) : Frama-C http://www.frama-c.com/ is an open-source
> industrial-strength code analysis platform developed at LSL. The recent
> plugin LTest http://micdel.fr/ltest.html builds on a combination of
> static and dynamic analysis in order to bring powerful automated testing
> abilities to the platform. The successful candidate will contribute to
> improve the LTest plugin through working in one of the following
> directions:
> . detection of infeasible test objectives through combination of
> static analyses
> . design of a (formal) language for specifying test objectives, and
> test automation through symbolic execution
>
>
> 3. Binary-level security analysis: The BINSEC project
> http://binsec.gforge.inria.fr/ aims at developing formal methods for
> binary-level security analysis, lifting previous work developed for
> safety analysis of critical systems. In this context, we are looking for
> a candidate willing to investigate the following topics, and integrate
> them into an open-source platform:
> . smart fuzzing and exploitability analysis
> . sound decompilation via static analysis
>
>
>
> * Context:
>
> Positions are up to 3-year long, to begin as soon as possible. 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 http://www.campus-paris-saclay.fr/en.
>
>
> * 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:
> - formal verification, and preferably software verification (static
> analysis, model checking, deductive verification, symbolic execution, etc.)
> - logic and the use of solvers in a verification setting
> - semantics of programming languages, compilation techniques
> - specification languages
> - security analysis, knowledge of architecture and/or assembly languages
> (3rd subject)
> - functional programming (OCaml)
>
>
> * Application:
>
> Applicants should send an email to Sébastien Bardin
> sebastien.bardin_at_cea.fr — including a CV, a motivation letter and
> 2-3 recommendation letters, and (depending on the subject) to Nikolai
> Kosmatov or to François Bobot firstname.lastname_at_cea.fr. More
> details on: http://sebastien.bardin.free.fr/2015-postdoc-positions.html
>