2025Activity reportProject-TeamSPADES
RNSR: 201321224T- Research center Inria Centre at Université Grenoble Alpes
- In partnership with:Université de Grenoble Alpes
- Team name: Sound Programming of Adaptive Dependable Embedded Systems
- In collaboration with:Laboratoire d'Informatique de Grenoble (LIG)
Creation of the Project-Team: 2015 July 01
Each year, Inria research teams publish an Activity Report presenting their work and results over the reporting period. These reports follow a common structure, with some optional sections depending on the specific team. They typically begin by outlining the overall objectives and research programme, including the main research themes, goals, and methodological approaches. They also describe the application domains targeted by the team, highlighting the scientific or societal contexts in which their work is situated.
The reports then present the highlights of the year, covering major scientific achievements, software developments, or teaching contributions. When relevant, they include sections on software, platforms, and open data, detailing the tools developed and how they are shared. A substantial part is dedicated to new results, where scientific contributions are described in detail, often with subsections specifying participants and associated keywords.
Finally, the Activity Report addresses funding, contracts, partnerships, and collaborations at various levels, from industrial agreements to international cooperations. It also covers dissemination and teaching activities, such as participation in scientific events, outreach, and supervision. The document concludes with a presentation of scientific production, including major publications and those produced during the year.
Keywords
Computer Science and Digital Science
- A1.1.1. Multicore, Manycore
- A1.1.9. Fault tolerant systems
- A1.3. Distributed Systems
- A2.1.1. Semantics of programming languages
- A2.1.6. Concurrent programming
- A2.1.9. Synchronous languages
- A2.3. Embedded and cyber-physical systems
- A2.3.1. Embedded systems
- A2.3.2. Cyber-physical systems
- A2.3.3. Real-time systems
- A2.3.5. Cyber-physical systems
- A4.5.3. Program proof
Other Research Topics and Application Domains
- B3.1. Sustainable development
- B4.5. Energy consumption
- B6.3.3. Network Management
- B6.6. Embedded systems
- B9. Society and Knowledge
1 Team members, visitors, external collaborators
Research Scientists
- Gregor Goessler [Team leader, INRIA, Senior Researcher, HDR]
- Martin Bodin [INRIA, Researcher]
- Pascal Fradet [INRIA, Researcher, HDR]
- Alain Girault [INRIA, Senior Researcher, HDR]
- Sophie Quinton [INRIA, Researcher]
- Jean-Bernard Stefani [INRIA, Senior Researcher]
Faculty Member
- Xavier Nicollin [GRENOBLE INP, Associate Professor]
Post-Doctoral Fellow
- Antoine Hardy [INRIA, Post-Doctoral Fellow, from Feb 2025]
PhD Students
- Baptiste De Goër De Herve [INRIA]
- Aurélie Kong Win Chang [INRIA, until May 2025]
- Alexander Obeid Guzman [INRIA]
Interns and Apprentices
- Timothe Baleras [INRIA, Intern, from Jun 2025 until Aug 2025]
- Henri Marion [UGA, Intern, from Jun 2025 until Aug 2025]
- Amaury Mazoyer [ENS DE LYON, Intern, from Jun 2025 until Jul 2025]
- Gregoire Stoupy [INRIA, Intern, from Jun 2025 until Aug 2025]
Administrative Assistants
- Julia Di Toro [INRIA]
- Nathalie Gillot [INRIA]
2 Overall objectives
The Spades project-team aims at contributing to meet the challenge of designing and programming dependable embedded systems in an increasingly distributed and dynamic context. Specifically, by exploiting formal methods and techniques, Spades aims to answer three key questions:
- How to program open distributed embedded systems as dynamic adaptive modular structures?
- How to program reactive systems with real-time and resource constraints?
- How to program fault-tolerant and explainable embedded systems?
These questions above are not new, but answering them in the context of modern embedded systems, which are increasingly distributed, open and dynamic in nature 53, makes them more pressing and more difficult to address: the targeted system properties – dynamic modularity, time-predictability, energy efficiency, and fault-tolerance – are largely antagonistic (e.g., having a highly dynamic software structure is at variance with ensuring that resource and behavioral constraints are met). Tackling these questions together is crucial to address this antagonism, and constitutes a key point of the Spades research program.
A few remarks are in order:
- We consider these questions to be central in the construction of future embedded systems, dealing as they are with, roughly, software architecture and the provision of real-time and fault-tolerance guarantees. Building a safety-critical embedded system cannot avoid dealing with these three concerns.
- The three questions above are highly connected. For instance, composability along time, resource consumption and reliability dimensions are key to the success of a component-based approach to embedded systems construction.
- For us, “Programming” means any constructive process to build a running system. It can encompass traditional programming as well as high-level design or “model-based engineering” activities, provided that the latter are supported by effective compiling tools to produce a running system.
- We aim to provide semantically sound programming tools for embedded systems. This translates into an emphasis on formal methods and tools for the development of provably dependable systems.
3 Research program
The SPADES research program is organized around three main themes, Design and programming models, Certified real-time programming, and Causality and reversibility, that seek to answer the three key questions identified in Section 2. We plan to do so by developing and/or building on programming languages and techniques based on formal methods and formal semantics (hence the use of “sound programming” in the project-team title). In particular, we seek to support design where correctness is obtained by construction, relying on proven tools and verified constructs, with programming languages and programming abstractions designed with verification in mind.
3.1 Design and Programming Models
Work on this theme aims to develop models, languages and tools to support a “correct-by-construction” approach to the development of embedded systems.
On the programming side, we focus on the definition of domain specific programming models and languages supporting static analyses for the computation of precise resource bounds for program executions. We propose dataflow models supporting dynamicity while enjoying effective analyses. In particular, we study parametric extensions and dynamic reconfigurations where properties such as liveness and boundedness remain statically analyzable. We also study the memory consumption of dataflow graphs. We study new techniques to find optimal sequential schedules (optimal in the sense that their memory peak is minimal) of task graphs and SDF graphs. We use these techniques to find parallel schedules that satisfy memory constraints, possibly the strongest ones.
On the design side, we focus on the definition of component-based models for software architectures combining distribution, dynamicity, real-time and fault-tolerant aspects. Component-based construction has long been advocated as a key approach to the “correct-by-construction” design of complex embedded systems 40. Witness component-based toolsets such as Ptolemy 33, BIP 29, or the modular architecture frameworks used, for instance, in the automotive industry (AUTOSAR) 27. For building large, complex systems, a key feature of component-based construction is the ability to associate with components a set of contracts, which can be understood as rich behavioral types that can be composed and verified to guarantee a component assemblage will meet desired properties.
Formal models for component-based design are an active area of research. However, we are still missing a comprehensive formal model and its associated behavioral theory able to deal at the same time with different forms of composition, dynamic component structures, and quantitative constraints (such as timing, fault-tolerance, or energy consumption).
We plan to develop our component theory by progressing on two fronts: a semantical framework and domain-specific programming models. The work on the semantical framework should, in the longer term, provide abstract mathematical models for the more operational and linguistic analysis afforded by component calculi. Our work on component theory will find its application in the development of a -based toolchain for the certified design and construction of dependable embedded systems, which constitutes our first main objective for this axis.
3.2 Certified Real-Time Programming
Programming real-time systems (i.e., systems whose correct behavior depends on meeting timing constraints) requires appropriate languages (as exemplified by the family of synchronous languages 30), but also the support of efficient scheduling policies, execution time and schedulability analyses to guarantee real-time constraints (e.g., deadlines) while making the most effective use of available (processing, memory, or networking) resources. Schedulability analysis involves analyzing the worst-case behavior of real-time tasks under a given scheduling algorithm and is crucial to guarantee that time constraints are met in any possible execution of the system. Reactive programming and real-time scheduling and schedulability for multiprocessor systems are old subjects, but they are nowhere as mature as their uniprocessor counterparts, and still feature a number of open research questions 28, 32, in particular in relation with mixed criticality systems. The main goal in this theme is to address several of these open questions.
We focus on two issues: multicriteria scheduling on multiprocessors, and schedulability analysis for real-time multiprocessor systems. Beyond real-time aspects, multiprocessor environments, and multicore ones in particular, are subject to several constraints in conjunction, typically involving real-time, reliability and energy-efficiency constraints, making the scheduling problem more complex for both the offline and the online cases. Schedulability analysis for multiprocessor systems, in particular for systems with mixed criticality tasks, is still very much an open research area.
Distributed reactive programming is rightly singled out as a major open issue in the recent, but heavily biased (it essentially ignores recent research in synchronous and dataflow programming), survey by Bainomugisha et al. 28. For our part, we focus on devising synchronous programming languages for distributed systems and precision-timed architectures.
3.3 Causality and Reversibility
Managing faults is a clear and present necessity in networked embedded systems. At the hardware level, modern multicore architectures are manufactured using inherently unreliable technologies 31, 38. The evolution of embedded systems towards increasingly distributed architectures highlighted in the introductory section means that dealing with partial failures, as in Web-based distributed systems, becomes an important issue.
In this axis we intend to address the question of how to cope with faults and failures in embedded systems? We will tackle this question by exploiting reversible programming models and by developing techniques for fault ascription and explanation in component-based systems.
A common theme in this axis is the use and exploitation of causality information. Causality, i.e., the logical dependence of an effect on a cause, has long been studied in disciplines such as philosophy 45, natural sciences, law 46, and statistics 47, but it has only recently emerged as an important focus of research in computer science. The analysis of logical causality has applications in many areas of computer science. For instance, tracking and analyzing logical causality between events in the execution of a concurrent system is required to ensure reversibility 43, to allow the diagnosis of faults in a complex concurrent system 39, or to enforce accountability 42, that is, designing systems in such a way that it can be determined without ambiguity whether a required safety or security property has been violated, and why. More generally, the goal of fault-tolerance can be understood as being to prevent certain causal chains from occurring by designing systems such that each causal chain either has its premises outside of the fault model (e.g., by introducing redundancy 35), or is broken (e.g., by limiting fault propagation 52).
4 Application domains
4.1 Industrial Applications
Our applications are in the embedded system area, typically: transportation, energy production, robotics, telecommunications, the Internet of things (IoT), systems on chip (SoC). In some areas, safety is critical, and motivates the investment in formal methods and techniques for design. But even in less critical contexts, like telecommunications and multimedia, these techniques can be beneficial in improving the efficiency and the quality of designs, as well as the cost of the programming and the validation processes.
Industrial acceptance of formal techniques, as well as their deployment, goes necessarily through their usability by specialists of the application domain, rather than of the formal techniques themselves. Hence, we are looking to propose domain-specific (but generic) realistic models, validated through experience (e.g., control tasks systems), based on formal techniques with a high degree of automation (e.g., synchronous models), and tailored for concrete functionalities (e.g., code generation).
4.2 Current Industrial Cooperations
Regarding applications and case studies with industrial end-users of our techniques, we cooperate with Orange Labs on software architecture for cloud services.
We are closely involved in Certisen, a startup project supported by ISS (Inria Startup Studio). The project focuses on Time-Sensitive Networking (TSN), which is the next generation of communication networks in critical sectors such as automotive, aerospace, and industrial systems. Certisen objective is to prove the correctness of TSN key properties (latency, priority, memory). A concrete tool, automatically extracted from Rocq/Coq proofs, will enable TSN configurations to be formally certified. This project is lead by Xiaojie Guo, a former PhD student of Spades. Pascal Fradet participates to Certisen as a technical adviser and by working on the formal specifications of TSN and Rocq proofs.
5 Social and environmental responsibility
5.1 Footprint of research activities
With the help of the GES 1point5 tool we have estimated the direct carbon footprint of our research activities in 2025. Our estimation is based on data gathered in a non-automated manner, as no tool automating the data extraction is available yet.
Professional travels, including the coming of jury members, amount to a total of 725 kg COe. Commute travels sum up to an estimated 1,5 t COe. We have purchased one computer, amounting for 192 kg COe. We roughly estimate our share of INRIA services and building usage to 6 t COe.
Based on the above estimations, our carbon footprint totals 8,4 t COe for the team, or an average of 765 kg COe per team member.
5.2 Impact of research results
Our research on certification and fault-tolerance aims at making embedded systems safer. Certified systems tend also to be simpler, less depending on updates and therefore less prone to obsolescence. A potential major application of causality analysis is to help establish liability for accidents caused by software errors.
On the other hand, our research may contribute to make more acceptable or even to promote many problematic systems such as IoT, drones, avionics, autonomous vehicles, ... with a potential negative environmental impact.
Sophie Quinton and Éric Tannier (from the BEAGLE team in Lyon), with the help of many colleagues, including some in the SPADES team, have set up a series of one-day workshops called “Ateliers SEnS” (for Sciences-Environnements-Sociétés), which offer a venue for members of the research community (in particular, but not limited to, researchers) to reflect on the social and environmental implications of their research. More than 50 Ateliers SEnS have taken place so far, all across France and beyond INRIA and the computer science field. Participants to a workshop can replicate it, and quite a few have already done so. Sophie Quinton has facilitated 2 Ateliers SEnS in 2025.
Research into the connection between ICT (Information and Communication Technologies) and the environmental crisis has started in 2020 within the SPADES team, see Section 7.4.
6 Latest software developments, platforms, open data
6.1 Latest software developments
6.1.1 CESAn
-
Name:
Core Erlang Semantics Analyzer
-
Keyword:
Formal semantics
-
Functional Description:
CESAn implements the semantics of a subset of Core Erlang. Given a Core Erlang program with finite semantics, it outputs its semantics in the form of a labeled transition system. The underlying small-step semantics faithfully represents message passing and signal handling in Erlang.
- Publications:
-
Contact:
Aurélie Kong Win Chang
-
Participants:
Aurélie Kong Win Chang, Jerome Feret, Gregor Goessler
6.1.2 MASTAG
-
Name:
Memory Analyzer and Scheduler for Task Graphs
-
Keyword:
Task scheduling
-
Functional Description:
The MASTAG software computes sequential schedules of a task graph or an SDF graph in order to minimize its memory peak.
MASTAG is made of several components: (1) a set of local transformations that compress a task graph while preserving its optimal memory peak, (2) an optimized branch and bound algorithm able to find optimal schedules for medium sized (30-50 nodes) task graphs, (3) support to accommodate SDF graphs in particular, their conversion into task graphs and a suboptimal technique to reduce their size.
MASTAG finds optimal sequential schedules in polynomial time for a wide range of directed acyclic task graphs (DAG), including trees and series-parallel DAG. On classic benchmarks, MASTAG always outperforms the state-of-the-art.
From an optimal sequential schedule, MASTAG can derive a dynamic parallel schedule satisfying any practical memory constraints and achieving good speedups. MASTAG is efficient and always succeeds in finding a parallel schedule that respects the required memory constraints, unlike alternative tools.
- URL:
-
Contact:
Alexandre Honorat
6.1.3 Tabvar
-
Keywords:
Coq, GUI (Graphical User Interface), Teaching
-
Functional Description:
This is a prototype of a graphical interface for the Coq proof assistant that includes graphical elements (here, curve sketching tabs). These elements are meant to interact with the usual textual proof of Coq, and help students learning how what a mathematical proof is expected to be.
- URL:
- Publication:
-
Contact:
Martin Bodin
-
Partner:
LIG
6.1.4 COSMetyc
-
Keyword:
OpenStreetMap
-
Functional Description:
This library can import, store, manipulate, and export OpenStreetMap data from and to various format of the community (like GeoJSON and OSM XML).
- URL:
-
Contact:
Martin Bodin
7 New results
7.1 Dataflow models of computation
Participants: Pascal Fradet, Alain Girault.
7.1.1 Memory minimization for dataflow graphs
Dataflow Models of Computation (MoCs) are widely used in embedded systems, including multimedia processing, digital signal processing, telecommunications, and automatic control. The reason is twofold. On the one hand the dataflow MoC is very close to classical block diagrams familiar to automatic control engineers. On the other hand it allows to nicely express the parallelism of an application, thereby allowing its efficient implementation on modern parallel architectures, be they multi-core processors or HPC platforms.
In 2022, we started focusing on optimizing the memory consumption of dataflow graphs, more precisely on the memory peak, defined as the maximum of the memory space used during the whole execution of the dataflow graph. This objective is critical both for embedded systems (due to the very small memory space available) and neural networks implemented in a dataflow fashion (due to the huge memory requirement). We have first proposed new techniques to find optimal sequential schedules of dataflow graphs, optimal in the sense that their memory peak is minimal. Then, we have studied how to find parallel schedules that satisfy memory constraints possibly the strongest ones.
We have proposed graph transformations that compress a task graph while preserving its optimal memory peak 18, 34. These transformations compress a large class of graphs into a single node representing their optimal schedule. In particular, we have formally proved that this is the case for all Series-Parallel Directed Acyclic Graphs (SP-DAGs). In addition, our graph transformations provide a simple characterization of optimal schedules for sets of independent tasks and allowed us to design an optimal compositional analysis dealing with single-source single-sink subgraphs (called S-T subgraphs). These S-T subgraphs can be analyzed separately and replaced by their best schedule. These results (correctness of the transformation rules, the compositional analysis, etc.) were formally proved. For graphs that cannot be compressed to a single node, we have designed an optimized branch and bound algorithm able to find optimal schedules for medium sized task graphs, between 30 and 50 nodes.
A natural extension of this work was to consider parallel schedules with shared memory, which we did in 2025. The optimal memory peak found for a sequential execution provides a lower bound for all its parallel versions. Thanks to a dynamic list scheduling algorithm under constraint, we are able to derive parallel schedules that are guaranteed to meet the desired memory peak constraint 22, even the harshest ones, whereas the previous state-of-the-art approaches mostly fail. To achieve this, we take advantage from the optimal sequential schedules from 18, 34. Furthermore, our approach is faster and can deal with very large task graphs, up to 50,000 tasks. When the constraints are the most severe (equal to the minimal memory peak), we still obtain very good speedups, respectively on 4 processors and on 8 processors on average. As expected, the more relaxed the memory constraints, the better the speedups become.
7.2 Real-time scheduling
Participants: Alain Girault.
7.2.1 Learning the speed policy for minimizing the energy consumption of hard real-time jobs
Since 2017, we have been working with Bruno Gaujal and Stephan Plassart on a very general model of real-time systems, made of a single-core processor equipped with DVFS1 and an infinite sequence of preemptive hard real-time jobs. Each real-time job is characterized by the triplet (inter-arrival time, size, relative deadline). The key point is that the system is clairvoyant without statistical knowledge, meaning that the job features are not known in advance, not even their probability distributions, but only revealed when the job is released. In this context, we wish to find the optimal speed policy, optimal meaning that all the jobs meet their deadline (hard real-time constraint) and that the average energy consumption is minimized. In 2025, we have proposed a machine learning method to learn the optimal speed policy, which consists of two successive phases. During the first phase, we observe the features of the incoming real-time jobs and we estimate their probability distribution. During this phase, the jobs are executed with the speed policy (OA) 54, which is known to be optimal when the future jobs are unknown. From this estimated probability distribution, we build and solve a constrained MDP (Markov Decision Process) and we compute the optimal speed policy (L), as in 37, 48, 36. Then the second phase starts, during which the jobs are executed with the learned speed policy (L). We have established a stopping criterion that gives the duration of the learning phase. Our experiments show that, after a learning period of 105 steps, our learned speed policy (L) is extremely close to the offline optimal one, with an error margin less than .
7.3 Causality and reversibility
Participants: Gregor Goessler, Jean-Bernard Stefani, Aurélie Kong Win Chang, Alexander Obeid Guzmán.
7.3.1 Causal explanations for embedded and concurrent systems
In order to pinpoint the root causes of system failures and explain why an observed outcome occurred, we have been developing techniques based on counterfactual analysis. Counterfactual analyses determine causal dependencies beyond those captured by classical causal semantics for concurrent systems. Given a system model, our goal is to extract the part of a failing execution trace that is causally relevant for the failure. We have been continuing our work on this topic in several directions.
We have developed a theory of explanations for discrete-event systems that allows us to analyze and compare different types of explanations by introducing a notion of semantics of an explanation. Based on this semantics we have formalised a set of expected properties for explanations, including completeness (all faulty traces can be explained) and precision (different faults have different explanations). We have then cast a frequently used type of explanation — called causal compression or subsequence explanation — in this framework and shown that it has no semantics that makes it both complete and precise. We have finally proposed a new type of explanations called choice explanation that focuses on branching choices in the execution of a system, and that satisfies our requirements.
Following up on Thomas Mari's PhD thesis 44, we are currently working on a symbolic construction of robustness functions for real-time systems, and its implementation, allowing us to effectively generate such explanations.
As part of the DCore project on causal debugging of concurrent programs, the goal of Aurélie Kong Win Chang's PhD thesis was to investigate the construction of causal explanations for Erlang programs. In 41 we have formalized a small step semantics for a subset of Core Erlang that models, in particular, its monitoring and signal systems. We have implemented this semantics in the Core Erlang Semantics Analyzer (CESAn 20, Section 6.1.1). Based on the semantics, the tool explains the causes of a program execution violating an expected safety property.
So far we assumed a system model to be known in order to assess causality. However, for many applications a faithful system model is not available. The goal of Alexander Obeid Guzman's PhD thesis is to leverage a measure of conditional algorithmic complexity in order to discover causal dependencies from the single observation of an execution trace coming from a distributed system.
7.4 Transversal activity: ICT and the Anthropocene
Participants: Martin Bodin, Baptiste De Goër De Herve, Pascal Fradet, Alain Girault, Gregor Goessler, Antoine Hardy, Xavier Nicollin, Sophie Quinton, Jean-Bernard Stefani.
Digital technologies are often presented as a powerful ally in the fight against climate change (see e.g., the discourse around the “convergence of the digital and the ecological transitions”), so we started research in this axis by investigating the potential of ICT for supporting the ecological transition. More generally, we are interested in the role played by ICT in the Anthropocene as well as new approaches to their design. This raises many complex challenges: For example, how do local measures meant to reduce the environmental impact of ICT relate (or not) to global effects? What can we learn from, and what are the limits of, current quantitative approaches for environmental impact assessment and their use for public debate and policy making? Which criteria could/should we take into account to design more responsible computer systems (other than efficiency, which is already well covered and subject to huge rebound effects in the case of digital technologies)? These questions require a systemic approach, and at least some basic knowledge of the state of the art in many scientific disciplines, in particular in STS (Science and Technology Studies).
Following recent work on these topics in the SPADES team (e.g., the PhD of Aina Rasoldier defended in 2024 50, 51, the internship of Ludmila Courtillat--Piazza in 2022 and the ongoing AEx SIA project in which we study how computer science should evolve to take into account the global changes brought about by the Anthropocene), two members of the SPADES team, namely Sophie Quinton and Jean-Bernard Stefani, have joined forces with other colleagues from Grenoble to launch a new Inria team named ADN for “Anthropocène et Décroissance du Numérique” (Anthropocene, Degrowth and ICT).
Work in the SIA project has progressed through the PhD thesis of Baptiste de Goër, which focuses on how ICT related sustainability issues are and could be taught in computer science classes. One major contribution was the study of how researchers problematize their work in the ICT4S conference community, and how nonepistemic values are involved 23. Another contribution is still in progress and relates to how CS high school teachers approach the environmental impacts of ICT in class and how to help them teach this complex question (initial results will be presented at the Didapro 2026 conference). In addition, in his postdoctoral work, Antoine Hardy has studied from a sociological perspective how the CS research community is coping with the ecological catastrophe. This work will be presented at the Archipel conference in 2026.
A second line of research on this topic relates to society's dependence on ICT, and focuses on the relation between the resilience of ICT infrastructures and the resilience of our societies in a future more and more constrained by the destabilization of planetary boundaries and its consequences on our social organisations. There has been so far no research on the potential consequences on the network performance of possible long term and continuous disruptions such as semiconductor shortages, for example due to shortages of raw material or environmental policy constraints. In a workshop paper, we study the resilience of mobile networks in the face of hardware aging and approach mobile network resilience using the stochastic geometry framework, proposing a network model including multiple dependent techno-bands (TB) and deriving approximate closed-form expressions for new resilience metrics. Numerical experiments show the influence of parameters such as load, base station density and the number of TB on network resilience. Another workshop paper presents how we intend to articulate a sociological survey with this CS modeling work.
A part of the ADN research proposal is centered on the notion of convivial technology initially proposed by the philosopher Ivan Illich in his book Tools for conviviality. We have argued in a paper entitled Conviviality for digital degrowth, to appear in the journal Philosophia Scientiae (as a follow up of 49), the relevance of conviviality for designing digital systems that are congruent with, and conducive to a degrowth society, and highlighted different research directions towards designing for conviviality and rethinking digital infrastructures and workflow systems.
7.5 Tooling up the teaching of proofs
Participants: Martin Bodin, Alain Girault.
Proof is a key concept in early licence degree in mathematics. It is known to be difficult to teach, due to its level of abstraction, but also due to the various roles it is meant to fulfill: it serves first to certify the mathematical statements themselves, but it also has a communication role and it intervenes within the research process (exploring the consequences of hypotheses, coming up with conjectures, etc.). Each of these roles requires different skills, and the licence's year comes with an increase of the required formalism. This makes it difficult but key to teach at this level.
The Spades team has long been working with the Rocq proof assistant, which provides a strong logical base for understanding proofs. It was thus natural for us to try to tool up licence's mathematical classes with Rocq. Mathematical classes have long been tooled up with computer software (like computer algebra systems or programming languages) to help providing intuitions or building conjectures. We want here to test whether a proof assistant can help teaching proof writing. This is the goal of the LiberAbaci project within Inria (which includes various other project-teams).
Within this project in Spades, we approached the IREMI institute, which brings together researchers and teachers to do research on mathematical teaching. We are also working with Julien Puydt, teacher in the Pupilles de l'Air high school.
We focus in reducing the entry cost of Rocq. Indeed, this software has originally been designed by and for experts, and not for math students. We thus explore several aspects in which it can be improved to more closely match the practice in math courses:
- We experiment with its interface to incorporate graphical components.
- We aim to ease the user interaction when writing proofs.
- We explore new ways in which mathematical notations can be defined.
- We seek for mechanisms to support a library of courses that scales and meet the need of teachers.
The use of graphical (and more generally non-textual) support within proofs in math courses is frequent, yet totally absent from Rocq. We thus sketched a new interface for the software that enables to incorporate such non-textual elements, and to be able to interact with them within a proof. The goal here is to be as close as possible to the current practice of teachers and students to reduce the entry cost of using the software. Our goal is not for the student to be able to use a proof assistant, but to help them produce better pen-and-paper proofs: the use of the proof assistant is here to guide them and help them understand what it expected and where. We are working on this subject with Emmanuel Beffara (LIG, team MeTAH) and Rémi Molinier (Institut Fourier). We are hoping to get an in-class experiment in 2026.
Proof assistants are heavily based on tactics, which are programs that can write parts of a proof: most of the user interaction with these tools are based on these tactics. We asked about 50 students at an early master's degree to solve a math problem and took their draft with their raw arguments. These students were chosen as they already had the abilities that we want to teach at the licence's level. They were also chosen by their relative diversity. We studied the arguments they used within their draft and categorised them on whether they were textual or not, on what the role each argument had in the overall proof they were (implicitly) building. We are designing tactics that follow as close as possible the students's arguments, and that could potentially guide them through the proof.
Math heavily relies on notations, that are frequently overloaded. For instance the symbol is both used as number multiplication, matrix multiplication, and cartesian product, although these operations are quite different. There already exists numerous mechanisms in Rocq to define notations and infer which instance of an overloaded symbol was meant to be used at a given point. We find these mechanisms incredible and they can be very useful in development. However, we fear that their error messages are difficult to understand by a non-expert: these systems tend to internally produce complex candidates that weren't always expected by the user, and their error messages tend to mention unfullfilled constraints for these complex candidates. We are thus working on much simpler mechanisms for notations that we expect to be closer to teachers's intuition. Such systems will be much less powerful than the state of the art, but we expect them to be more aligned with teaching. We are working in collaboration with Julien Puydt (Pupilles de l'Air) and Arthur Charguéraud (Inria, Camus team).
Still with the help of Julien Puydt, we are looking for mechanisms to build library content that could scale. Building libraries is known to be an intensive task, and current mathematical libraries in Rocq are from time to time subject to large-scale refactoring. This is due to their structure from the ground-up: each mathematical notion is built on smaller ones, and each change in an inner structure can impact all the ones on top of it. We fear that this library structure isn't the perfect fit for teachers. First, teachers usually lack the time to maintain content up to date with external changes. Second, this library structure doesn't follow the natural order of a course: monoids are taught after groups, but monolithic libraries tend to define groups with the help of monoids, in the reverse order. We are thus currently assessing what features teachers would need to design a mathematical library for teaching. Once identified, we plan to implement these features, or to relate them with existing features.
8 Bilateral contracts and grants with industry
Participants: Jean-Bernard Stefani.
8.1 Bilateral contracts with industry
- Inria and Orange Labs have established in 2015 a joint virtual research laboratory, called I/O Lab. We have been heavily involved in the creation of the laboratory and are actively involved in its operation (Jean-Bernard Stefani was one of the two co-directors of the lab, till Feb. 2020). I/O Lab focuses on the network virtualization and cloudification. As part of the work of I/O Lab, we have cooperated with Orange Lab, as part of a cooperative research contract funded by Orange, on the verification of system configurations in cloud computing environments and software-defined networks.
9 Partnerships and cooperations
9.1 National initiatives
9.1.1 Défi Inria
LiberAbaci
Participants: Martin Bodin.
LiberAbaci is a project between Inria project teams Cambium, Camus, Gallinette, , Spades, Stamp, Toccata, and the Laboratoire d'Informatique de Paris-Nord. The overall objective is to study how one could use the proof assistant in a Mathematical course in the University to help teaching proofs. At Spades, Martin Bodin is working with the IREMI at Grenoble to involve math teachers and didactic researchers to the project.
SmartNet
Participants: Gregor Goessler, Alexander Obeid Guzman.
The SmartNet project, kicked off in 2024, aims to develop network management techniques to handle the increasing complexity of networks. In particular, SmartNet seeks to provide comprehensive insights of the network and its subsystems by identifying cause-effect relationships, enabling strategic interventions for malfunction prevention. We collaborate in this project with the APTIKAL team from LIG, and Nokia Research. This project funds Alexander Guzmán's PhD thesis as well as the postdoc position of Nishchal Prasad, who is hosted by the APTIKAL team and co-advised by Gregor Goessler.
SIA
Participants: Baptiste De Goër, Sophie Quinton.
The SIA Exploratory Research project, supported by INRIA's DGDS, funds the PhD work of Baptiste de Goër and provides funding for an upcoming postdoctoral fellow in Sciences and Technology Studies. The goal of the project is to provide interdisciplinary foundations for studying the complex relationship between computer science, information and communication technologies (ICT), society and the environment. We approach the problem from three complementary perspectives: 1) by contributing to an interdisciplinary overview of the state of knowledge on the environmental impacts of ICT; 2) by studying the complex connection between computer science and the Anthropocene through the way it is and could be taught in secondary schools; 3) by exploring, at a local scale, the possibility to deploy frugal or low tech alternatives to existing digital systems, following a participatory approach.
10 Dissemination
Participants: Martin Bodin, Pascal Fradet, Alain Girault, Gregor Goessler, Xavier Nicollin, Sophie Quinton, Jean-Bernard Stefani.
10.1 Promoting scientific activities
10.1.1 Scientific events: organisation
General chair, scientific chair
- Alain Girault was co-chair of the International Workshop on Synchronous Programming (SYNCHRON’25).
Member of the organizing committees
- Alain Girault is a member of the Steering Committee of the Embedded Systems Week (ESWEEK).
- Martin Bodin is a member of the Steering Committee for Didapro'11.
- In connection to the CIS-PEN working group and the Persyval-Lab ICT-S research axis, Sophie Quinton co-organized two national scientific events in Grenoble, "Numérique et soutenabilité, quels usages de la modélisation ?" and "Regards croisés sur les infrastructures numériques et numérisées", as well as a panel "Regards croisés sur les enjeux et limites de la quantification environnementale du numérique" at the Journées Scientifiques du CIS.
10.1.2 Scientific events: selection
Chair of conference program committees
Sophie Quinton is a co-chair for the Undone Computer Science 2026 conference.
Member of the conference program committees
- Alain Girault was TPC member of the Forum on Description Languages international conference (FDL’25) and the Time-Centric Reactive Software international workshop (TCRS'25).
- Sophie Quinton was a TPC member of the SCW 2026 workshop.
10.1.3 Journal
Member of the editorial boards
- Alain Girault is associate editor for the EURASIP Journal on Embedded Systems and for the Real-Time Systems Journal.
- Gregor Goessler has been a guest editor of the IST special issue on Causal modeling and inference in software engineering 25.
Reviewer - reviewing activities
- Alain Girault reviewed a paper for ACM Transactions on Parallel Computing.
- Martin Bodin reviewed a paper for ICFP.
10.1.4 Invited talks
Sophie Quinton was invited to panels at GRETSI 2025, Réparer le Futur (rencontres inter-AtEcoPol 2025) and the Journée d'Étude "Enjeux environnementaux du numérique au prisme des SHS". She gave an invited talk at a workshop on “IA et recherche en santé”.
10.1.5 Leadership within the scientific community
Sophie Quinton co-chairs a working group of the GDR CIS associated with the Center for Internet and Society focused on environmental issues. She also co-chairs the “ICT and sustainability” Persyval-lab axis.
10.1.6 Scientific expertise
Sophie Quinton is a member of the scientific board of Grenoble Métropole and the Agence d'urbanisme de la région grenobloise.
10.1.7 Research administration
- Since October 2013, Pascal Fradet has been head of the committee for doctoral studies (“Responsable du comité des études doctorales”) of the Inria Grenoble research center. He is also the local correspondent for the young researchers Inria mission (“Mission jeunes chercheurs”) and serves as the substitute of the director of the Inria Grenoble research center at the doctoral school council (MSTII).
- Up to June 2025, Alain Girault was Deputy Scientific Director at INRIA, in charge of the domain “Algorithmics, Programming, Software and Architecture”' (51 research teams over 9 INRIA research centers).
- Gregor Goessler is a member of the Scientific policy committee (COS) of the Inria Grenoble center, of the council of the MSTIC department of Grenoble University, and of the scientific jobs committee at Inria Grenoble.
- Sophie Quinton facilitated until the end of 2025 the SEnS-GRA group which hosts discussions and proposes actions regarding the environmental and societal impact of our research at Inria Grenoble.
10.2 Teaching - Supervision - Juries - Educational and pedagogical outreach
10.2.1 Teaching
- Licence: Pascal Fradet, Modèles de Calcul: -calcul, CM & TD, 30 H eqTD, level L3, Univ. Grenoble Alpes, France.
- Licence: Alain Girault, Modèles de Calcul: -calcul, TD, 18 H eqTD, level L3, Univ. Grenoble Alpes, France.
- Licence: Martin Bodin, Modèles de Calcul: -calcul, TD, 18 h eqTD, level L3, Univ. Grenoble Alpes, France.
- Licence: Martin Bodin, Langage et traducteurs, Programmation Fonctionnelle, TP, 30 h eqTD, level M1, Polytech Grenoble, France.
- Master : Sophie Quinton, Numérique responsable, 15 HeqTD, level M1, Grenoble INP (Ensimag), France.
- Sophie Quinton gave a one-day course at the EJCP Summerschool, contributed to the scientific program and gave two lectures at the AI autumn school, gave one lecture and attended one panel at the Ensimag engineering school, and gave a lecture at the ENS Lyon CS departement seminar.
10.2.2 Supervision
- Gregor Goessler, PhD completed: Aurélie Kong Win Chang, “Causal explanations for concurrent programs in Erlang”'; co-advised by Gregor Goessler and Jérôme Feret.
- Gregor Goessler, PhD in progress: Alexander Obeid Guzmán, “Inference of causal models for networks from single observations”; since January 2024.
- Sophie Quinton, PhD in progress: Baptiste de Goër, “Teaching ICT-related sustainability issues in computer science courses”.
- Sophie Quinton, PhD in progress: Ludmila Courtillat–Piazza, “Dépendance au numérique et vulnérabilités dans un contexte d’urgence écologique, abordées sous l’angle de la résilience des réseaux mobiles”.
10.2.3 Juries
Sophie Quinton, member of the PhD committee of Simon Delarue, Telecom Paris.
10.2.4 Educational and pedagogical outreach
Sophie Quinton contributed to the serious game PhoneImpact.
10.3 Popularization
10.3.1 Specific official responsibilities in science outreach structures
- Martin Bodin serves as a local correspondant for the Chiche! program.
10.3.2 Participation in Live events
- Martin Bodin animated an activity on logic during the science festival « Fête de la science ».
- Sophie Quinton gave a lecture on the environmental impacts of ICT at a high school event.
11 Scientific production
11.1 Major publications
- 1 articleERPOT: A Quad-Criteria Scheduling Heuristic to Optimize Execution Time, Reliability, Power Consumption and Temperature in Multicores.IEEE Transactions on Parallel and Distributed Systems3010October 2019, 2193-2210HALDOI
- 2 articleA Predictable Framework for Safety-Critical Embedded Systems.TC637The complete PRET-C reference.July 2014, 1600--1612
- 3 articleA Survey of Parametric Dataflow Models of Computation.ACM Trans. Design Autom. Electr. Syst.2222017, 38:1--38:25DOI
- 4 articleAspects preserving properties.Science of Computer Programming7732012, 393-422
- 5 articleGraph Transformations for Memory Peak Minimization by Scheduling.ACM Transactions on Embedded Computing Systems (TECS)2024, 1-36In press. HAL
- 6 articleRDF: A Reconfigurable Dataflow Model of Computation.ACM Transactions on Embedded Computing Systems (TECS)December 2022HALDOI
- 7 inproceedingsCertiCAN: A Tool for the Coq Certification of CAN Analysis Results.RTAS 2019 - 25th IEEE Real-Time and Embedded Technology and Applications SymposiumMontreal, CanadaIEEEApril 2019, 1-10HALDOI
- 8 articleCertiCAN : Certifying CAN Analyses and Their Results.Real-Time Systems592March 2023, 160-198HALDOI
- 9 inproceedingsFormal Analysis of Timing Effects on Closed-loop Properties of Control Software.35th IEEE Real-Time Systems Symposium 2014 (RTSS)Rome, ItalyDecember 2014HAL
- 10 articleSafety Controller Synthesis for Incrementally Stable Switched Systems Using Multiscale Symbolic Models.IEEE Transactions on Automatic Control6162016, 1537-1549HALDOI
- 11 articleA general framework for blaming in component-based systems.Science of Computer Programming113, Part 32015HALDOI
- 12 articleCausality analysis and fault ascription in component-based systems.Theoretical Computer Science8372020, 158-180HALDOI
-
13
articleReversibility in the higher-order
-calculus.Theoretical Computer Science6252016, 25-84HALDOI - 14 inproceedingsFormal analysis of sporadic overload in real-time systems.2012 Design, Automation & Test in Europe Conference & Exhibition, DATE 2012, Dresden, Germany, March, 20122012, 515--520URL: http://dx.doi.org/10.1109/DATE.2012.6176523DOI
- 15 inproceedings How realistic are claims about the benefits of using digital technologies for GHG emissions mitigation? LIMITS 2022 - Eighth Workshop on Computing within Limits Virtual, France June 2022 HAL
- 16 inproceedingsA Formal Link Between Response Time Analysis and Network Calculus.ECRTS 2022 - 34th Euromicro Conference on Real-Time SystemsModene, ItalyJuly 2022HALDOI
11.2 Publications of the year
International journals
Invited conferences
International peer-reviewed conferences
National peer-reviewed Conferences
Edition (books, proceedings, special issue of a journal)
Doctoral dissertations and habilitation theses
11.3 Cited publications
- 27 miscAutomotive Open System Architecture.2003, URL: http://www.autosar.orgback to text
- 28 articleA Survey on Reactive Programming.ACM Computing Surveys4542013back to textback to text
- 29 articleRigorous Component-Based System Design Using the BIP Framework.IEEE Software2832011back to text
- 30 articleThe synchronous languages 12 years later.Proceedings of the IEEE9112003back to text
- 31 articleDesigning Reliable Systems from Unreliable Components: The Challenges of Transistor Variability and Degradation.IEEE Micro2562005back to text
- 32 articleA Survey of Hard Real-Time Scheduling for Multiprocessor Systems.ACM Computing Surveys4342011back to text
- 33 articleTaming heterogeneity - the Ptolemy approach.Proceedings of the IEEE9112003back to text
- 34 inproceedingsSequential Scheduling of Dataflow Graphs for Memory Peak Minimization.Proceedings of the 24th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES '23)Orlando (FL), United StatesACMJune 2023, 76-86HALDOIback to textback to text
- 35 articleFundamentals of Fault-Tolerant Distributed Computing in Asynchronous Environments.ACM Computing Surveys3111999back to text
- 36 articleAn MDP-Based Solution for the Energy Minimization of Non-Clairvoyant Hard Real-Time Systems.Real-Time SystemsDecember 2024, 47HALDOIback to text
- 37 articleDynamic Speed Scaling Minimizing Expected Energy Consumption for Real-Time Tasks.Journal of SchedulingJuly 2020, 1-25HALDOIback to text
- 38 inproceedingsArchitectures for Online Error Detection and Recovery in Multicore Processors.Design Automation and Test in Europe (DATE)2011back to text
- 39 incollectionDiagnosis with Petri Net Unfoldings.Control of Discrete-Event Systems433Lecture Notes in Control and Information SciencesSpringer2013, 15back to text
- 40 inproceedingsThe Embedded Systems Design Challenge.Formal Methods 20064085Lecture Notes in Computer ScienceSpringer2006back to text
- 41 inproceedingsA Semantics of Core Erlang with Handling of Signals.Erlang 2023 - 22nd ACM SIGPLAN International Workshop on ErlangSeattle WA, United StatesACMSeptember 2023, 31-38HALDOIback to text
- 42 inproceedingsAccountability: definition and relationship to verifiability.ACM Conference on Computer and Communications Security2010, 526-535back to text
- 43 inproceedingsReversing Higher-Order Pi.21th International Conference on Concurrency Theory (CONCUR)6269Lecture Notes in Computer ScienceSpringer2010back to text
- 44 phdthesisCausal explanations for reactive real-time systems.Université Grenoble - AlpesNovember 2023HALback to text
- 45 incollectionCounterfactual Theories of Causation.Stanford Encyclopedia of PhilosophyStanford University2009, URL: http://plato.stanford.edu/entries/causation-counterfactualback to text
- 46 bookCausation and Responsibility.Oxford1999back to text
- 47 articleCausal inference in statistics: An overview.Statistics Surveys32009, 96-146back to text
- 48 phdthesisOnline optimization in dynamic real-time systems.Université Grenoble Alpes [2020-....]June 2020HALback to text
- 49 inproceedingsTaking conviviality seriously (extended abstract).2024 - 1st conference on Undone Science in Computer ScienceNantes, FranceFebruary 2024, 1-4HALback to text
- 50 phdthesisComment évaluer le potentiel d'une solution numérique face à l'urgence écologique ? Application aux plateformes de covoiturage régulier à l'échelle locale.Université Grenoble Alpes [2020-....]February 2024HALback to text
- 51 inproceedingsAssessing the Potential of Carpooling for Reducing Vehicle Kilometers Traveled.International Conference on Information and Communications Technology for Sustainability, ICT4S'23Rennes, FranceIEEEJune 2023, 120--131HALDOIback to text
- 52 techreportPartitioning for Safety and Security: Requirements, Mechanisms, and Assurance.CR-1999-209347NASA Langley Research Center1999back to text
- 53 miscARTEMIS Strategic Research Agenda.2011back to text
- 54 inproceedingsA scheduling model for reduced CPU energy.Proceedings of lEEE Annual Foundations of Computer Science1995, 374--382back to text