[TYPES/announce] 2-year Postdoc Position on Frama-C/E-ACSL

[Julien Signoles]

Hello,

The Software Reliability and Security Lab at CEA LIST (Paris Saclay, 
France) is hiring a 2-year postdoctoral researcher to improve the 
Frama-C runtime verification plug-in E-ACSL.

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 adapt existing 
compilation techniques or define new 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:
- OCaml programming (at least, functional programming)
- C programming
- runtime verification
- compilation
- static analysis
- semantics of programming languages
- formal specification

A full description of the position is available online:

     http://julien.signoles.free.fr/positions/postdoc-eacsl.pdf

Feel free to contact me for additional details,
Julien Signoles
-- 
Researcher-engineer
CEA LIST, Software Reliability and Security Lab
tel:(+33)1.69.08.00.18 fax:(+33)1.69.08.83.95 Julien.Signoles at cea.fr