VLDB 2026 Research / reviewers in the wild / expert
Mikaël Briday
dblp:09/5309
· DBLP profile ↗
12ranked-venue papers
0as first author
7since 2021 · last 2025
0000-0001-7251-6688ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Systems, architecture and hardware · 6 · 3 since 2021Software engineering, systems software and programming languages · 3 · 2 since 2021Theory of computation · 2 · 1 since 2021Security and privacy · 1 · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Circadia: Checkpointing for Intermittent Computing in AI Driven ApplicationsabstractBattery-less embedded systems powered by energy harvesting eliminate the need for battery maintenance and enable their deployment in remote environments. However, their intermittent execution, disrupted by unpredictable power failures, complicates data processing. Solutions for intermittency management gravitate around one key technique: checkpointing volatile data before power failures, and retrieving data at system reboot. Moreover, since data transmission is a major source of energy consumption, performing computations directly ondevice is essential. Initially used for simple tasks such as goods identifications, battery-less systems are now being applied to more energy-intensive tasks such as image recognition leveraging machine learning algorithms such as Convolutional Neural Networks (CNNs). In this paper, we introduce Circadia, a checkpointing strategy dedicated to CNN inference in battery-less systems. By leveraging the structured dataflow and control flow of CNNs, Circadia strategically places checkpoints within the CNN code to ensure task termination, data consistency, and low energy consumption. By design, Circadia has a linear complexity relative to model size, a significant improvement over the closest state-of-the-art checkpointing method, which has cubic complexity. This enables Circadia to handle much larger CNNs. Experimental results, on both generated and state-of-the-art embedded CNNs, show that its checkpoint placement time is several orders of magnitude lower than existing approaches, while its energy consumption at runtime remains nearly identical. Matthieu Rodet, Jean-Luc Béchennec, Mikaël Briday, Sébastien Faucou, Isabelle Puaut, Erven Rohou |
DSD | 3 |
| 2025 | A Study in Specification and Hardware Runtime Verification of Critical Embedded SoftwareabstractWe evaluate HARVEST (Hardware Accelerated Runtime Verification for Embedded SofTware), a runtime error detection mechanism for embedded software running on standard SoPC architectures,i.e., one (or more) processor(s) and an FPGA on a single chip. The program under monitoring runs on the processor(s), while a trace analysis module running on the FPGA detects errors in its execution. The hardware implementation of trace analysis minimizes the performanceimpact and achieves a very low error reporting latency (a few processor cycles). In this article, we evaluate the suitability of using HARVEST to detect errors resulting from transient physical faults. We explain how HARVEST is used to monitor a complex software component (Trampoline RTOS) on a commercially available hardware platform (Microchip SmartFusion2). We measure the overhead of the resulting instrumentation on system resources. We then evaluate its performance in detecting silent data corruptions, based on a systematic simulation of bit flips at the instruction set architecture level. We report a detection rate of up to 90.2% for a fairly low system resource overhead, suggesting an interesting trade-off for designers of highly constrained critical systems. Dimitry Solet, Jean-Luc Béchennec, Mikaël Briday, Sébastien Faucou, Sébastien Pillement |
IEEE Trans. Dependable Secur. Comput. | 3 |
| 2024 | SCHEMATIC: Compile-Time Checkpoint Placement and Memory Allocation for Intermittent SystemsabstractBattery-free devices enable sensing in hard-to-access locations, opening up new opportunities in various fields such as healthcare, space, or civil engineering. Such devices harvest ambient energy and store it in a capacitor. Due to the unpredictable nature of the harvested energy, a power failure can occur at any time, resulting in a loss of all non-persistent information (e.g., processor registers, data stored in volatile memory). Checkpointing volatile data in non-volatile memory allows the system to recover after a power failure, but raises two issues: (i) spatial and temporal placement of checkpoints; (ii) memory allocation of variables between volatile and non-volatile memory, with the overall objective of using energy as efficiently as possible. While many techniques rely on the developer to address these issues, we present Schematic,a compiler technique that automates checkpoint placement and memory allocation to minimize the overall energy consumption. Schematicensures that programs will eventually terminate (forward progress property). Moreover, checkpoint placement and memory allocation adapt to the size of the energy buffer and the capacity of volatile memory. Schematictakes advantage of volatile memory (VM) to reduce the energy consumed, by automatically placing the most used variables in VM. We tested Schematicfor different experimental settings (size of volatile memory and capacitor) and results show an average energy reduction of 51 % compared to related techniques. Hugo Reymond, Jean-Luc Béchennec, Mikaël Briday, Sébastien Faucou, Isabelle Puaut, Erven Rohou |
CGO | 3 |
| 2024 | EarlyBird: Energy belongs to those who wake up earlyabstractBy relying on ambient energy, battery-less devices significantly increase the autonomy of IoT devices, enabling maintenance-free operation in remote locations. However, due to the scarcity of ambient energy, these devices rely on capacitors to buffer energy, and alternate between power-off phases where the device is harvesting energy and computation bursts. In most existing techniques, the device resumes execution only when the capacitor is full. However, we argue that doing so is sub-optimal. Instead, we advocate that waking-up the device sooner may yield better performance since the microcontroller consumes less power when operating at lower voltage. To this extent, we introduce EarlyBird, a technique that automatically computes a fine-tuned wake-up voltage for each resume point. EarlyBird leverages static analysis to determine how much energy is needed before resuming from a given program location, and provides a runtime library to enforce the early wake-up strategy. We evaluated how EarlyBird improves existing checkpointing techniques and results show an increase in the number of benchmarks executed per minute of up to 5.65×. Hugo Reymond, Jean-Luc Béchennec, Mikaël Briday, Sébastien Faucou, Isabelle Puaut, Erven Rohou |
RTCSA | 3 |
| 2023 | Securing a RISC-V architecture: A dynamic approachabstractThe SecureV (also known as SecV) project offers an innovative, open-source hardware, secure, and high-performance processor core based on the RISC-V ISA. The originality of the approach lies in the integration of a complete solution to increase security based on dynamic code transformation, covering 4 of the 5 NIST11National Institute of Standards and Technology functions of cybersecurity via monitoring (identify, detect), obfuscation (protect), and dynamic adaptation (react). Sébastien Pillement, Maria Mendez Real, J. Pottier, T. Nieddu, Bertrand Le Gal, Sébastien Faucou, Jean-Luc Béchennec, Mikaël Briday, Sylvain Girbal, Jimmy Le Rhun, Olivier Gilles, Daniel Gracia Pérez, André Sintzoff, Jean-Roch Coulon |
DATE | 8 |
| 2021 | Timed Petri Nets with Reset for Pipelined Synchronous Circuit Design
Rémi Parrot, Mikaël Briday, Olivier H. Roux |
Petri Nets | 2 |
| 2021 | Pipeline Optimization using a Cost Extension of Timed Petri NetsabstractA major step in arithmetic operators design is the placement of pipeline stages, with the goal of drastically increase the data throughput. Approaches, such as the as-soon-as-possible greedy algorithm, allow pipelining with a frequency target. They can possibly be combined with a retiming operation to reduce the number of pipeline registers. This retiming step is based on a weighted directed graph model, from which the pipeline placement is reduced to an optimisation problem (for example ILP). However, this approach produces only a unique solution, and makes it difficult to add additional constraints on the resulting pipeline. We propose to use a Timed Petri Net extension with cost, where time captures the propagation delay and cost measures the size of pipeline registers. The state space of the model captures exactly the circuit states and the branching points, so its exploration can be guided by comparing the circuit states regarding any feature (number and size of registers, critical path, throughput, etc). The pipeline exploration can be reduced to a weighted branching-time logic model-checking problem, that we prove to be PSPACE-complete on this model. We have implemented this exploration algorithm in a prototype tool. We apply it on some arithmetic operators provided by FloPoCo showing improvements up to 35% compared to the current implementation. Rémi Parrot, Mikaël Briday, Olivier H. Roux |
ARITH | 2 |
| 2017 | WCET Analysis by Model Checking for a Processor with Dynamic Branch Prediction
Armel Mangean, Jean-Luc Béchennec, Mikaël Briday, Sébastien Faucou |
VECoS | 3 |
| 2014 | Reactive embedded device driver synthesis using logical timed models
Julien Tanguy, Jean-Luc Béchennec, Mikaël Briday, Olivier H. Roux |
SIMULTECH | 3 |
| 2013 | Device driver synthesis for embedded systemsabstractCurrently the development of embedded software managing hardware devices that fulfills industrial constraints (safety, real time constraints) is a very complex task. To allow an increased reusability between projects, generic device drivers have been developed in order to be used in a wide range of applications. Usually the level of gener-icity of such drivers require a lot of configuration code, which is often generated. However, a generic driver requires a lot of configuration and need more computing power and more memory needs than a specific driver. This paper presents a more efficient methodology to solve this issue based on a formal modeling of the device and the application. Starting from this modeling, we use well-known game theory techniques to solve the driver model synthesis problem. The resulting model is then translated into the actual driver embedded code with respect to an implementation model. By isolating the model of the device, we allow more reusability and interoperability between devices for a given application, while generating an application-specific driver. Julien Tanguy, Jean-Luc Béchennec, Mikaël Briday, Sebastien Dube, Olivier H. Roux |
ETFA | 3 |
| 2012 | Harmless, a hardware architecture description language dedicated to real-time embedded system simulation
Rola Kassem, Mikaël Briday, Jean-Luc Béchennec, Guillaume Savaton, Yvon Trinquet |
J. Syst. Archit. | 2 |
| 2006 | Trampoline An Open Source Implementation of the OSEK/VDX RTOS SpecificationabstractThis paper introduces an OSEK/VDX operating system implementation. OSEK/VDX is an industry standard for real-time operating system used in the field of automotive embedded software. This implementation is proposed in the context of the open source software, which interest needs not to be demonstrated any more. The paper explains the main implementation choices as well as the technique proposed for the generation of a real-time application. This implementation is nowadays available for three targets: Infineon C167, Darwin/PowerPC and Linux/x86. Jean-Luc Béchennec, Mikaël Briday, Sébastien Faucou, Yvon Trinquet |
ETFA | 2 |