Skip to content
Snippets Groups Projects
Commit 8d676701 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'internships/internship-ml4eva-2023' into 'master'

[jobs] Add internship position on ml4eva.

See merge request !166
parents d2ec3ac3 5c85c88e
No related branches found
No related tags found
1 merge request!166[jobs] Add internship position on ml4eva.
Pipeline #50415 passed
---
layout: job
title: Internship Position at CEA LIST - LSL
short_title: Internship Position
short: Deep Learning for improving formal verification with Frama-C / Eva
date: 04-11-2022
filled: false
keywords: Deep Learning, Graph Neural Networks , Representation Learning, Static analysis, Formal methods
---
# {{ page.short }}
Institution
-----------
The French [Alternative Energies and Atomic Energy Commission](https://www.cea.fr/) (CEA) is a key
player in research, development, and innovation. Drawing on the widely
acknowledged expertise gained by its 16,000 staff spanned over 9 research
centers with a budget of 4.1 billion Euros, CEA actively participates in more
than 400 European collaborative projects with a large number of academic
(notably as a member of [Paris-Saclay University](https://www.universite-paris-saclay.fr))
and industrial partners. Within the CEA Technological Research Division, the
[CEA List](https://www-list.cea.fr) institute addresses the challenges coming from smart digital systems.
Among other activities, CEA List's Software Safety and Security
Laboratory (LSL) research teams design and implement automated
analysis in order to make software systems more trustworthy, to
exhaustively detect their vulnerabilities, to guarantee conformity to
their specifications, and to accelerate their certification. In
particular, the [Frama-C platform](https://frama-c.com/) is dedicated to perform
a wide range of analyses over C programs (with an experimental C++ front-end).
Objectives
----------
Inside Frama-C, the Eva plugin provides several static analysis techniques
dedicated to the automatic inference of program properties and, in particular,
runtime errors (arithmetic overflows, invalid memory accesses and other C
undefined behaviors). These techniques are efficiently combined, but their
activation can be expensive in terms of resource consumption (time and memory).
It is therefore necessary to choose wisely which techniques to use in which
case.
These choices are now made by the analyst, who uses the tool to perform safety
proofs on a software. They require a detailed knowledge of of Frama-C and its
analysis techniques, both of which evolve with time. Moreover, to be as fine as
possible, these choices can be made at the function or loop level in a sometimes
large source code. This double difficulty, based on both the quantity of
knowledge and the time needed, can be a blocking obstacle.
To remove this obstacle, we have implemented promising machine-learning
techniques. This involves treating the difficulty no longer as a problem of
understanding the analysis tool but as a problem of understanding the relation
between code patterns and the different analysis techniques. This has two
advantages. On the one hand, the learning can be repeated as the tool evolves,
in order to to remain adapted to the characteristics of the latest available
techniques. On the other hand, the automatic choice of techniques can be done at
a much finer level level than what a human can accomplish in a reasonable time.
The objectives of the internship are to contribute to our machine-learning
toolchain specialized on source code, to participate in its integration in
Frama-C, and to improve its performance in the automatic selection of analysis
strategies. Several internship directions are possible:
- Investigate and develop specialized learning techniques on graphs (in
particular, Graph Neural Networks),
- Explore learning techniques in the presence of unbalanced data
- Study and develop a distributed version of the toolchain capable of fully
leveraging the resources of our cluster FactoryIA.
All positions include theoritical research as well as prototyping and
experimental evaluation.
Qualifications
--------------
- **Minimal**
- Final-year master student in Computer Science or Computer Enginnering
- Solid ability in Python programming
- Solid ability with deep learning frameworks (TensorFlow or PyTorch)
- ability to work in a team
- **Preferred**
- A certain taste for mathematical matters
- Some knowledge of functional programming, preferably OCaml
- Some knowledge of imperative programming, preferably C
Characteristics
---------------
- **Duration:** 5-6 months
- **Location:** [CEA Nano-INNOV](https://www.openstreetmap.org/#map=19/48.71238/2.19335), Paris-Saclay Campus, France
- **Compensation:**
- €700 to €1300 monthly stipend (determined by CEA compensation grids)
- maximum €229 housing and travel expense monthly allowance (in case a relocation is needed)
- CEA buses in Paris region and 75% refund of transit pass
- subsidized lunches
## Application
If you are interested in this internship, please send to the [contact
persons](#contact-persons) an application providing the following information:
- Your resume;
- A cover letter indicating how your curriculum and experience match the
qualifications expected and how you would plan to contribute to the project
- Your bachelor and master transcripts
- The contact details of two persons (at least one academic) who can be
contacted to provide references.
Applications are welcomed until the position is filled. Please note that the
administrative processing may take up to **3 months**, so we encouraged
interested students to take contact as soon as possible.
## Contact persons
For further information or details about the internship before applying, please contact:
- Michele Alberti (<michele.alberti@cea.fr>)
- Valentin Perrelle (<valentin.perrelle@cea.fr>)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment