This page is dedicated to positions related to Frama-C. If one of the topic below interests you, please send a motivation letter, a CV and whatever information you deem relevant to the indicated contact.
This page may be incomplete: if you would like to do interesting and innovative development and/or research in the Frama-C team, feel free to contact us. It is useful to start with background knowledge in one or several of:
The aim of this internship is to define, to formalize, to prove correct and finally to implement a static dataflow analysis which helps to reduce the amount of generated code made by a code generator.
The aim of this internship is to use Frama-C for reporting alarms according to CWE's classification. This covers two main aspects. First, existing alarms have to be associated with the appropriate CWE number. Second, some extensions to Frama-C will have to be devised in order to cover more CWE categories than what can be reached by the current implementation. Ideally, at the end of the internship, Frama-C should be in position to qualify for the CWE compatibility program.
The aim of this internship is to find and evaluate open-source case studies using the Value Analysis plug-in. This includes the following tasks: (1) finding suitable code bases for the Value Analysis plug-in, based on available open-source code; (2) parameterizing the analysis to minimize false alarms; (3) trying to identify real weaknesses/bugs on the code, to report them; (4) measuring and classifying the results, e.g. which kinds of code are better analyzed, which parameters are more relevant, etc.
The aim of this internship is to develop methods to analyse accurately and with minimum cost programs manipulating arrays into Frama-C. It would start with state of the art algorithms, their evaluation within the Frama-C framework and lead to new propositions.