Postdoc on Runtime Verification at CEA LIST, Université Paris-Saclay, France

Dear all,

The Software Safety and Security Lab at CEA LIST, Université Paris-Saclay, France has 2 open postdoc positions in the area of runtime verification for code safety and security:

• Designing Compilation Techniques for Improving Efficiency of E-ACSL, a Runtime Assertion Checker for C Programs http://julien-signoles.fr/positions/postdoc-eacsl.pdf

• Control Flow Integrity for Remote Attestation http://julien-signoles.fr/positions/postdoc-cfi.pdf

The candidates will:

• Solve challenging research problems;
• Implement their results in Frama-C, an industrial-strength open-source framework for analyses of C code;
• Evaluate their solutions on concrete benchmarks or/and use cases;
• Publish their results in international conferences and journals.

Strong knowledge in at least one of the following areas is welcome:

• Programming
  • OCaml and C
  • Formal semantics
• Formal verification
  • Runtime verification, static analysis, formal specification languages, …
• Compilation
  • Code generation, program transformation, type system, …

Interested applicants should send a CV and a motivation letter to Julien Signoles (julien dot signoles at cea dot fr).

Best regards, Julien Signoles