Frama-C is a collaborative platform for analysis of C programs. Among the different tools available in Frama-C, WP is dedicated to deductive verification of programs, allowing mathematical proof of functional properties and absence of runtime errors. This tool is used for years in industry.

Separation logic is the most promising way to allow verification of properties for programs involving complex data structures. However, it is hard to use for industrial use-cases. The main reason for this is that it is hard to encode into automatic proof tools. Thus, its use requires a lot of work from users.

The WP tool of Frama-C does not use separation logic. An ongoing research project aims at integrating elements from separation logic into WP, in order to improve performances and the ability to deal with complex data-structures. However, the proposed extension does not allow verifying programs with recursive data-structures, for this, we need the representation precidates from separation logic. The goal of this postdoc is to study how to integrate them in WP.

The post-doctoral fellow will be in charge of the development of specific numerical tools for multivariate analysis, to perform the reduction, processing and analysis of massive data acquired by Diffraction/Scattering Computed Tomography (DSCT) on synchrotron beamlines. Two aspects will be treated: the reconstruction of tomographic data, and the development of statistical classification tools for spectral data. The latter will be also applied to the analysis of X-ray absorption spectroscopy (XAS) data. The post-doctoral fellow will work mainly on the MARS beamline at SOLEIL synchrotron, and will benefit from the close collaboration between MARS and CEA/IRESNE/DEC researchers who are experts in multi-scale characterization of materials. At the end of this work, the teams of the CEA and the MARS beamline will thus have new innovative tools for the analysis of massive data, in support of their future DSCT and XAS experiments, in particular for the fine characterization of spent nuclear fuel.

Within a multidisciplinary technological research team of experts in SW/HW co-design tools by applying formal methods, you will be involved in a national research project aiming at developing an environment to identify, analyze and reduce the interferences generated by the concurrent execution of applications on a heterogeneous commercial-off-the-shelf (COTS) multi-core hardware platform.

One of the main goals of modern reactor physics is to perform accurate multi-physics simulations of the behaviour of a nuclear reactor core, with a detailed description of the geometry at the fuel pin level. Multi-physics calculations in nominal conditions imply a coupling between a transport equation solver for the neutron and precursor populations, thermal and thermal-hydraulics solvers for heat transfer, and a Bateman solver for computing the isotopic depletion of the nuclear fuel during a reactor cycle. The purpose of this post-doc is to carry out such a fully-coupled calculation using the PATMOS Monte Carlo neutron-transport mini-app and the C3PO coupling platform, both developed at CEA. The target system is core of the size of a commercial reactor.

This post-doctoral subject concerns the development of Monte-Carlo ray-tracing methods for modeling radiation heat transfer in the context of severe accidents. Starting from a well-developed software framework for Monte Carlo simulation of particle transport in the context of reactor physics and radiation protection, we will seek to adapt existing methods to the problem of radiative heat transfer, in a high-performance computing framework. To do this, we will develop a hierarchy of approximations associated with radiative heat transfer that are intended to allow the validation of simplified models implemented in the context of the numerical simulation of severe accidents in nuclear reactors. Focusing on algorithm and simulation performance, this work is intended to be a "proof of principle" of the possible software mutualization around the Monte-Carlo method for particle transport on the one hand and radiative heat transfer on the other hand.

One of the main challenges in the deployment of robotics in industry is to offer smart robots, capable of understanding the context in which they operate and easily programmable without advanced skills in robotics and computer science. In order to enable a non-expert operator to define tasks subsequently carried out by a robot, the CEA is developing various tools: intuitive programming interface, learning by demonstration, skill-based programming, interface with interactive simulation, etc.

Winner of the "moonshot" call for projects from the CEA's Digital Missions, the "Self-learning robot" project proposes to bring very significant breakthroughs for the robotics of the future in connection with simulation. A demonstrator integrating these technological bricks is expected on several use cases in different CEA centers.

This post-doc offer concerns the implementation of the CEA/DES (Energy Department) demonstrator on the use case of laser cutting under constraints for A&D at the Simulation and Dismantling Techniques Laboratory (LSTD) at the CEA Marcoule.

Modern computers offer the possibility to use Monte-Carlo codes to get reference solutions to neutron transport problems. Nevertheless, such reference solutions are only accessible in stationary conditions for practical problems.

The proposed research work aims at exploring and testing methods to obtain a reference Monte-Carlo solution for fuel cycle quantities in depletion problems using present-day computing resources. Such a reference, obtained at a reasonable computational cost, would provide a better control over calculation biases and uncertainties in deterministic solutions typically used in the industry.

Studies will be performed using the Monte Carlo code TRIPOLI-4® coupled with the MENDEL deterministic depletion module. The post-doctoral fellow will perform extensive work on neutron leakage consideration in order to ensure criticality of the model, neutron flux and reaction rates normalization, control of the energy deposition in the different model regions, fine descriptions of the irradiation history, cross section stochastic temperature interpolation, as well as the impact of considering only a limited number of isotopes. Comparisons will be made with the results published by other groups using different approaches and Monte-Carlo codes .

The post-doctoral fellow will be positioned in a team of researchers/engineers in nuclear reactor physics. He/she will improve and deepen his/her knowledge of applied Monte-Carlo simulations as well as the code validation process.