User Tools

  • Logged in as: anonymous (anonymous)
  • Logout

Site Tools


mantis:frama-c:positions

Open positions

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:

  • formal methods
  • static analysis
  • software safety
  • software security
  • OCaml programming
  • theorem proving

Postdoctoral positions

Phd theses

Internships

Static Analysis for Optimizing a Code Generator (Master's)

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.

Contacts are Julien Signoles and Nikolaï Kosmatov. More information is available (in French) here, or in English upon request.

Generation of counter-examples (Master's)

The aim of this internship is to develop a Frama-C plug-in that uses WP and external provers to generate examples leading to an alarm emitted by Value Analysis, showing that the alarm is a true one.

Contact is Virgile Prevosto. More information is available (in French) here, or in English upon request.

Using Frama-C for verifying absence of CWEs (Master's)

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.

Contacts are Virgile Prevosto, Julien Signoles and Armand Puccetti. More information is available here, or in English upon request.

Studying open-source C programs with the Value plug-in (Master's)

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.

Contacts are Andre Maroneze and Boris Yakobowski. More information is available here, or in English upon request.

Improving a Static Analyzer for programs manipulating Arrays (Master's)

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.

Contacts are Valentin Perrelle and Matthieu Lemere. More information is available here, or in English upon request.

mantis/frama-c/positions.txt · Last modified: 2017/01/25 14:52 by yakobowski