Frama-C is a code analysis platform for C programs which provides several collaborative analyzers as plug-ins. It allows the user to annotate C programs with formal specifications written in the ACSL specification language in order to verify them statically or dynamically. Static analysis techniques may be used on a partial program, that is a program containing external library functions, as soon as they are specified enough. However dynamic analysis techniques like monitoring or testing cannot be used on such partial programs because they cannot be executed. The aim of this postdoc is to address this limitation by automatically generating a C function body ‘b’ from an ACSL function contract ‘c’ in a way that ‘b’ satisfies ‘c’. Such a code generation is named function synthesis in the litterature. The postdoc will adapt existing works to C programs annotated with ACSL annotations and will improve state-of-the-art techniques to handle new kinds of annotations. Then a full compilation scheme will be designed and proved correct. Finally it will be implemented in OCaml as a new Frama-C plug-in and experimented on a realistic case study.

This position is open until it is filled.

Département: Département Ingénierie Logiciels et Systèmes (LIST)
Laboratory: Laboratoire pour la Sûreté du Logiciel
Start Date: 01-06-2015
ECA Code: PsD-DRT-15-0038
Contact: Julien.Signoles<στο>cea.fr