34 citations · 119 across the 18 of their papers we have counts for
20 papers
An Efficient Summation Algorithm for the Accuracy, Convergence and Reproducibility of Parallel Numerical Methods
Farah Benmouhoub, Pierre-Loïc Garoche, Matthieu Martel
Nowadays, parallel computing is ubiquitous in several application fields, both in engineering and science. The computations rely on the floating-point arithmetic specified by the I…
Verification and Validation of Convex Optimization Algorithms for Model Predictive Control
Raphaël Cohen, Eric Féron, Pierre-Loïc Garoche
Advanced embedded algorithms are growing in complexity and they are an essential contributor to the growth of autonomy in many areas. However, the promise held by these algorithms…
Bounding Fixed Points of Set-Based Bellman Operator and Nash Equilibria of Stochastic Games
Sarah H. Q. Li, Assalé, Adjé +2
Motivated by uncertain parameters encountered in Markov decision processes (MDPs) and stochastic games, we study the effect of parameter uncertainty on Bellman operator-based algor…
Parabolic Set Simulation for Reachability Analysis of Linear Time Invariant Systems with Integral Quadratic Constraint
Paul Rousse, Pierre-Loïc Garoche, Didier Henrion
This work extends reachability analyses based on ellipsoidal techniques to Linear Time Invariant (LTI) systems subject to an integral quadratic constraint (IQC) between the past st…
Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Guillaume Davy, Eric Féron, Pierre-Loïc Garoche +1
Classical control of cyber-physical systems used to rely on basic linear controllers. These controllers provided a safe and robust behavior but lack the ability to perform more com…
Foundations of Intelligent Additive Manufacturing
Kévin Garanger, Eric Feron, Pierre-Loïc Garoche +4
During the last decade, additive manufacturing has become increasingly popular for rapid prototyping, but has remained relatively marginal beyond the scope of prototyping when it c…
Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems
Victor Magron, Pierre-Loic Garoche, Didier Henrion +1
We consider the problem of approximating the reachable set of a discrete-time polynomial system from a semialgebraic set of initial conditions under general semialgebraic set const…
Hierarchical State Machines as Modular Horn Clauses
Pierre-Loïc Garoche, Temesghen Kahsai, Xavier Thirioux
In model based development, embedded systems are modeled using a mix of dataflow formalism, that capture the flow of computation, and hierarchical state machines, that capture the…
Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization
Assalé Adjé, Pierre-Loïc Garoche, Victor Magron
While abstract interpretation is not theoretically restricted to specific kinds of properties, it is, in practice, mainly developed to compute linear over-approximations of reachab…
A Sums-of-Squares Extension of Policy Iterations
Assalé Adjé, Pierre-Loïc Garoche, Victor Magron
In order to address the imprecision often introduced by widening operators in static analysis, policy iteration based on min-computations amounts to considering the characterizatio…
Synthesizing Modular Invariants for Synchronous Code
Pierre-Loic Garoche, Arie Gurfinkel, Temesghen Kahsai
In this paper, we explore different techniques to synthesize modular invariants for synchronous code encoded as Horn clauses. Modular invariants are a set of formulas that characte…
Quadratic Zonotopes:An extension of Zonotopes to Quadratic Arithmetics
Assalé Adjé, Pierre-Loïc Garoche, Alexis Werey
Affine forms are a common way to represent convex sets of using a base of error terms . Quadratic forms are an extension of affine forms enabling the u…
Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs
Assalé Adje, Pierre-Loïc Garoche
Among the various critical systems that worth to be formally analyzed, a wide set consists of controllers for dynamical systems. Those programs typically execute an infinite loop i…
From Design to Implementation: an Automated, Credible Autocoding Chain for Control Systems
Timothy Wang, Romain Jobredeaux, Heber Herencia +4
This article describes a fully automated, credible autocoding chain for control systems. The framework generates code, along with guarantees of high level functional properties whi…
Invariant stream generators using automatic abstract transformers based on a decidable logic
Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli
The use of formal analysis tools on models or source code often requires the availability of auxiliary invariants about the studied system. Abstract interpretation is currently one…
Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
The actor model eases the definition of concurrent programs with non uniform behaviors. Static analysis of such a model was previously done in a data-flow oriented way, with type s…
Thermodynamic investigation of an insulator irradiated by a low-energy electron beam
F. Pesty, P. Garoche
The surface of an insulating material irradiated by a beam of low energy electrons charges positively if the yield of secondary electron is greater than unity. For such a dynamical…
Background discrimination capabilities of a heat and ionization germanium cryogenic detector
P. Di Stefano, L. Berge, B. Chambon +26
The discrimination capabilities of a 70 g heat and ionization Ge bolometer are studied. This first prototype has been used by the EDELWEISS Dark Matter experiment, installed in the…
Event categories in the EDELWEISS WIMP search experiment
A. Benoit, L. Berge, A. Broniatowski +28
Four categories of events have been identified in the EDELWEISS-I dark matter experiment using germanium cryogenic detectors measuring simultaneously charge and heat signals. These…
Status of the EDELWEISS Experiment
L. Berge, I. Berkes, B. Chambon +20
The status of the EDELWEISS experiment (underground dark matter search with heat-ionisation bolometers) is reviewed. Auspicious results achieved with a prototype 70 g Ge heat-ionis…