diff --git a/_jobs/2022-11-04-internship-ml4eva.md b/_jobs/2022-11-04-internship-ml4eva.md new file mode 100644 index 0000000000000000000000000000000000000000..234dbdab4fc6b764ef9ac067b8af112777e82828 --- /dev/null +++ b/_jobs/2022-11-04-internship-ml4eva.md @@ -0,0 +1,128 @@ +--- +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>)