Internship position H/F

Job description: Although formal verification is essential for ensuring the safety and security of software, it remains difficult to deploy and use effectively by non-experts due to its steep learning curve. Recent advances in large language models (LLMs) have demonstrated remarkable abilities in code understanding, synthesis, and reasoning. These advances open promising research directions for assisting developers and verification engineers in formal specification and verification tasks. The goal of this internship is to explore and evaluate the integration of LLMs assistance into the Frama-C environment to support and automate parts of the specification and verification workflow. The work will focus on identifying the extent to which LLMs can provide meaningful support without compromising the rigor and reliability of formal program analysis. The following topics represent potential research and technical directions of the internship. Depending on the interests of the intern, one or more of them will be pursued, or other directions might be devised as the internship progresses. Automatic Specification Synthesis: Use LLMs to infer program specifications, selecting an appropriate formalism (e.g., ACSL, MetAcsl, RPP), and explore strategies to evaluate the robustness of synthesized specifications themselves, e.g., using Frama-C’s infrastructure or counterexample-based refinement. Assistance in Verification Configuration: Design mechanisms for LLMs to suggest appropriate Frama-C plugins (e.g., Wp, Eva, E-ACSL, RTE) and configurations or parameters based on the characteristics of the analyzed code and objectives. Assessment and Prioritization of Verification Results: When potential issues are reported, develop an LLM-assisted process to classify their severity and likelihood of exploitation, providing a prioritized and interpretable view of verification results, potentially in combination with Frama-C’s results themselves. All these potential directions raise several challenges at the intersection of software engineering, artificial intelligence, and formal methods. Integration Challenge: Setting up an environment where LLMs can interact programmatically with Frama-C, interpret analysis feedback, and refine their outputs iteratively. This can build upon the Loupe framework. Reliability and Hallucination Control: Designing mechanisms to detect, quantify, and reduce hallucinations or incorrect inferences produced by the model, possibly through cross-validation against Frama-C’s analysis results. Evaluation Metrics: Defining criteria for assessing the quality and usefulness of AI-generated specifications and test cases, both in terms of correctness and their impact on verification coverage. Human-AI Collaboration: Studying how AI-generated suggestions can be presented to the user to maximize productivity and trust, ensuring the expert remains in control of final verification decisions.

Institute description: The French Alternative Energies and Atomic Energy Commission (CEA) is a key player in research, development, and innovation. Drawing on the widely acknowledged expertise gained by its 20,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) and industrial partners. Within the CEA Technological Research Division, the CEA List 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 is dedicated to perform a wide range of analyses over C programs (with an experimental C++ front-end).

Your profile: RequiredInterest in AI-assisted software engineering Willingness to explore interactions between LLMs and formal verification frameworks Solid knowledge of Python and its ecosystem Ability to work in a team PreferredFamiliarity with machine learning and large language models, including prompt design or API integration. Familiarity with the Frama-C platform. Some knowledge of the OCaml and C programming languages

Level of qualification studied: Bac+5 - Master 2

Languages: English Fluent,French Fluent