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: