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.

Combining Array Abstraction Techniques for Static Analysis

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.

Contact is Valentin Perrelle. More information is available here, or in English upon request.

Verification of Quantum Programs by Abstract Intepretation

Since quantum programs are hard to test, simulate or debug, the aim of this internship is to explore the potential of Abstract Interpretation for the verification of quantum programs. The internship would start by looking on an existing technique to find entanglement properties and then explore on either more high-level properties or on well-formedness of quantum programs.

Contacts are Valentin Perrelle, Sébastien Bardin and Benoît Valiron. More information is available here, or in English upon request.

mantis/frama-c/positions.txt · Last modified: 2018/01/10 13:58 by valentin.perrelle