A formal framework for the specification and verification of distributed processes communication flows in clouds
Clouds are constituted of servers interconnected via the Internet, on which systems can be implemented, making use of applications and databases deployed on the servers. Cloud-based computing is gaining in popularity, and that includes the context of critical systems. As a result, it is useful to define formal frameworks for reasoning about cloud-based systems. One requirement about such a framework is that it enables reasoning about the concepts manipulated in a cloud, which naturally includes the ability to reason about distributed systems, composed of subsystems deployed on different machines and interacting through message passing to implement services. In this context, the ability to reason about communication flows is central. The aim of this thesis is to define a formal framework dedicated to the specification and verification of systems deployed on clouds. This framework will capitalize on the formal framework of "interactions". Interactions are models dedicated to the specification of communication flows between different actors in a system. The thesis work will study how to define structuring (enrichment, composition) and refinement operators to enable the implementation of classical software engineering processes based on interactions.
Co-Design of Ultra-Compact Integrated Converters Leveraging Solid-State Micro-Batteries
Improving the performance of DC-AC and AC-DC power conversion systems is key to reducing system weight, extending operational autonomy, and enhancing compactness. This PhD project aims to explore novel topologies of integrated power converters by leveraging an emerging component: solid-state micro-batteries.
The research will begin with a system-level study of two representative applications — one AC-DC and one DC-AC — to define the constraints and opportunities offered by solid-state batteries. The candidate will then identify and co-optimize the most suitable converter topology for ultra-low power operation (in the milliwatt range) in conjunction with a matrix of available micro-batteries. The work will culminate in the design, fabrication, and experimental validation of the proposed architecture.
Co-supervised by Dr. Gaël Pillonnet (CEA-Leti, France) and Prof. Patrick Mercier (University of California, USA), the candidate will join a cutting-edge research environment focused on advanced Power Management Integrated Circuits (PMICs). This project offers a strong application-oriented dimension, targeting the co-optimization of circuits and emerging micro-storage components within ultra-compact systems, such as micro-motor actuation and micro-powering from mains voltage.
Joining our team means contributing to the advancement of disruptive technologies with high potential impact in fields such as healthcare, defense, and predictive maintenance.
Anisotropic approaches in graph signal processing. Application to graph neural networks.
Signal processing on graphs is based on the properties of an elementary operator generally associated with a notion of random walk / diffusion process. One limitation of these approaches is that the operator is systematically isotropic, a property that is passed on to any notion of filtering based on it. In multi-dimensional signal processing (images, video, etc), on the other hand, non-isotropic filters (or even filters that only take one direction into account) are used extensively, which greatly increases the possibilities. These non-isotropic filters are, in particular, the basic element of convolutional neural networks, which would likely have poorer performance with isotropic filters alone (i.e. impulse response with circular/spherical symmetry). The isotropy of the filters is also currently considered to be a major obstacle to the expressiveness of convolutional neural networks on graphs, which could be overcome using non-isotropic signal processing constructions on graphs. In addition to homogeneous graphs, operators used for signal processing or neural networks on bipartite or more generally heterogeneous graphs also have this property of isotropy where the neighbours of a node are treated identically. Although this time there is no obvious link with classical approaches, the notion of anisotropic or directional operator also seems relevant here to differentiate processing according to the multiple facets that can contribute to a given relationship.
To approach the concept of directionality in graphs, we will rely on the fact that a graph can often be viewed as a discretization of a Riemannian manifold. We will also examine extensions to bipartite graphs, which share similarities with a relationship between two manifolds, as well as heterogeneous graphs composed of multiple relations. Applications to graph neural networks will be explored to investigate the flexibility gained through directionality.
Bridging the embedding gap between expressive specification and efficient verification of machine learning
Formal verification of neural networks is facing a double-faceted issue. The expressiveness of specifications (as in: compact and close to human understanding) is apparently clashing with their efficient translation to state-of-the-art prover, who only support a fragment of arithmetic without quantifiers.
This thesis will investigate "global" properties. Such class of properties describe generic behaviours of neural networks, beyond the level of local samples. Such properties are currently partially specified and most of them cannot be soundly derived into standard prover queries. Using the expressive power of the WhyML specification langage, this thesis will strive to propose a common encoding for global properties and investigate their efficient compilation to prover queries thanks to automated graph editing techniques.
This thesis will also investigate the comparison of provers performance, in particular drawing inspiration from portfolio approaches.
Long-term and non-invasive plant monitoring using MIR spectroscopy
The LCO (french acronym for Optical Sensors Laboratory) develops innovative Silicium integrated photonic components (optical sources, waveguides, photodetectors, etc), sensors, and eventually systems. From upstream technological research to industrial transfers, those sensors apply in various fields such as environment, health, and security.
One of the laboratory research topic is mid-infrared spectroscopy of dense samples, using a photothermal detection technology. As we got convincing results applying our sensors for monitoring humans physiological parameters, we now wish to adapt them to plants. First laboratory trials reveal encouraging results, but their interpretation is at this stage out of reach because of the complexity of the measure, and the case study itself. Tackling this problematic is the thesis objective.
To achieve it, the candidate will establish an experimental program with the help of instrumentation and plant biology specialists. He will have access to the laboratory computational and experimental resources, as well as the CEA-Grenoble prototyping capabilities.
GenPhi : 3D Generative AI conditioned by geometry, structure and physics
The aim of this thesis is to design new 3D model generators based on Generative Artificial Intelligence (GenAI), capable of producing faithful, coherent and physically viable shapes. While 3D generation has become essential in many fields, current automatic generation approaches suffer from limitations in terms of respecting geometric, structural and physical constraints. The goal is to develop methods for integrating constraints related to geometry, topology, internal structure and physical laws, both stationary (equilibrium, statics) and dynamic (kinematics, deformation), right from the generation stage. The study will combine geometric perception, semantic enrichment and physical simulation approaches to produce robust, realistic 3D models that can be directly exploited without human intervention.
Towards Reliable and Autonomous Workflow Coordination in Agentic AI-Based Systems
The rise of Large Language Models (LLMs) and agentic AI systems is transforming how complex workflows are designed and managed. Unlike traditional centralized orchestration, modern workflows must support distributed, autonomous agents operating across cloud, edge, and on-premise environments. These agents collaborate with humans and other systems, adapt to evolving goals, and cross organizational and trust boundaries. This paradigm shift is especially relevant in domains like cybersecurity and healthcare emergency response, where workflows must be dynamically constructed and executed under uncertainty. In such settings, rigid automation falls short—agentic workflows require decentralized, secure, and auditable orchestration.
This thesis explores how to enable such systems, asking: How can we achieve secure, distributed orchestration in environments where agentic AI operates autonomously? It will propose a formal modeling framework for distributed agentic workflows, protocols for auditable, privacy-preserving coordination, and a reference architecture with real-world proofs of concept in cybersecurity and healthcare.
Robust and Secure Federated Learning
Federated Learning (FL) allows multiple clients to collaboratively train a global model without sharing their raw data. While this decentralized setup is appealing for privacy-sensitive domains like healthcare and finance, it is not inherently secure: model updates can leak private information, and malicious clients can corrupt training.
To tackle these challenges, two main strategies are used: Secure Aggregation, which protects privacy by hiding individual updates, and Robust Aggregation, which filters out malicious updates. However, these goals can conflict—privacy mechanisms may obscure signs of malicious behavior, and robustness methods may violate privacy.
Moreover, most research focuses on model-level attacks, neglecting protocol-level threats like message delays or dropped updates, which are common in real-world, asynchronous networks.
This thesis aims to explore the privacy–robustness trade-off in FL, identify feasible security models, and design practical, secure, and robust protocols. Both theoretical analysis and prototype implementation will be conducted, leveraging tools like Secure Multi-Party Computation, cryptographic techniques, and differential privacy.
AI Enhanced MBSE framework for joint safety and security analysis of critical systems
Critical systems must simultaneously meet the requirements of both Safety (preventing unintentional failures that could lead to damage) and Security (protecting against malicious attacks). Traditionally, these two areas are treated separately, whereas they are interdependent: An attack (Security) can trigger a failure (Safety), and a functional flaw can be exploited as an attack vector.
MBSE approaches enable rigorous system modeling, but they don't always capture the explicit links between Safety [1] and Security [2]; risk analyses are manual, time-consuming and error-prone. The complexity of modern systems makes it necessary to automate the evaluation of Safety-Security trade-offs.
Joint safety/security MBSE modeling has been widely addressed in several research works such as [3], [4] and [5]. The scientific challenge of this thesis is to use AI to automate and improve the quality of analyses. What type of AI should we use for each analysis step? How can we detect conflicts between safety and security requirements? What are the criteria for assessing the contribution of AI to joint safety/security analysis?
Physics informed deep learning for non-destructive testing
This PhD project lies within the field of Non-Destructive Testing (NDT), which encompasses a range of techniques used to detect defects in structures (cables, materials, components) without causing any damage. Diagnostics rely on physical measurements (e.g., reflectometry, ultrasound), whose interpretation requires solving inverse problems, which are often ill-posed.
Classical approaches based on iterative algorithms are accurate but computationally expensive, and difficult to embed for near-sensor, real-time analysis. The proposed research aims to overcome these limitations by exploring physics-informed deep learning approaches, in particular:
* Neural networks inspired by traditional iterative algorithms (algorithm unrolling),
* PINNs (Physics-Informed Neural Networks) that incorporate physical laws directly into the learning process,
* Differentiable models that simulate physical measurements (especially reflectometry).
The goal is to develop interpretable deep models in a modular framework for NDT, that can run on embedded systems. The main case study will focus on electrical cables (TDR/FDR), with possible extensions to other NDT modalities such as ultrasound. The thesis combines optimization, learning, and physical modeling, and is intended for a candidate interested in interdisciplinary research across engineering sciences, applied mathematics, and artificial intelligence.