BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Pierre-Loïc Garoche

Pierre-Loïc Garoche contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
math.OCLogic in Computer ScienceComputation and LanguageFormal Languages and Automata TheorySystems and ControlComputer Science and Game Theoryeess.SYSoftware Engineering

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
8works
0followers
8topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

8 published item(s)

preprint2022arXiv

An Efficient Summation Algorithm for the Accuracy, Convergence and Reproducibility of Parallel Numerical Methods

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 IEEE754 Standard. In this context, an elementary brick of computation, used everywhere, is the sum of a sequence of numbers. This sum is subject to many numerical errors in floating-point arithmetic. To alleviate this issue, we have introduced a new parallel algorithm for summing a sequence of floating-point numbers. This algorithm which scales up easily with the number of processors, adds numbers of the same exponents first. In this article, our main contribution is an extensive analysis of its efficiency with respect to several properties: accuracy, convergence and reproducibility. In order to show the usefulness of our algorithm, we have chosen a set of representative numerical methods which are Simpson, Jacobi, LU factorization and the Iterated power method.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Fixed Points of the Set-Based Bellman Operator

Motivated by uncertain parameters encountered in Markov decision processes (MDPs), we study the effect of parameter uncertainty on Bellman operator-based methods. Specifically, we consider a family of MDPs where the cost parameters are from a given compact set. We then define a Bellman operator acting on an input set of value functions to produce a new set of value functions as the output under all possible variations in the cost parameters. Finally we prove the existence of a fixed point of this set-based Bellman operator by showing that it is a contractive operator on a complete metric space.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Parabolic Set Simulation for Reachability Analysis of Linear Time Invariant Systems with Integral Quadratic Constraint

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 state and disturbance signals , interpreted as an input-output energetic constraint. To compute the reachable set, the LTI system is augmented with a state corresponding to the amount of energy still available before the constraint is violated. For a given parabolic set of initial states, the reachable set of the augmented system is overapproximated with a time-varying parabolic set. Parameters of this paraboloid are expressed as the solution of an Initial Value Problem (IVP) and the overapproximation relationship with the reachable set is proved. This paraboloid is actually supported by the reachable set on so-called touching trajectories. Finally , we describe a method to generate all the supporting paraboloids and prove that their intersection is an exact characterization of the reachable set. This work provides new practical means to compute overapproximation of reachable sets for a wide variety of systems such as delayed systems, rate limiters or energy-bounded linear systems.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Verification and Validation of Convex Optimization Algorithms for Model Predictive Control

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 cannot be kept without proper attention to the considerably stronger design constraints that arise when the applications of interest, such as aerospace systems, are safety-critical. Formal verification is the process of proving or disproving the ''correctness'' of an algorithm with respect to a certain mathematical description of it by means of a computer. This article discusses the formal verification of the Ellipsoid method, a convex optimization algorithm, and its code implementation as it applies to receding horizon control. Options for encoding code properties and their proofs are detailed. The applicability and limitations of those code properties and proofs are presented as well. Finally, floating-point errors are taken into account in a numerical analysis of the Ellipsoid algorithm. Modifications to the algorithm are presented which can be used to control its numerical stability.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization

While abstract interpretation is not theoretically restricted to specific kinds of properties, it is, in practice, mainly developed to compute linear over-approximations of reachable sets, aka. the collecting semantics of the program. The verification of user-provided properties is not easily compatible with the usual forward fixpoint computation using numerical abstract domains. We propose here to rely on sums-of-squares programming to characterize a property-driven polynomial invariant. This invariant generation can be guided by either boundedness, or in contrary, a given zone of the state space to avoid. While the target property is not necessarily inductive with respect to the program semantics, our method identifies a stronger inductive polynomial invariant using numerical optimization. Our method applies to a wide set of programs: a main while loop composed of a disjunction (if-then-else) of polynomial updates e.g. piecewise polynomial controllers. It has been evaluated on various programs.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Quadratic Zonotopes:An extension of Zonotopes to Quadratic Arithmetics

Affine forms are a common way to represent convex sets of $\mathbb{R}$ using a base of error terms $ε\in [-1, 1]^m$. Quadratic forms are an extension of affine forms enabling the use of quadratic error terms $ε_i ε_j$. In static analysis, the zonotope domain, a relational abstract domain based on affine forms has been used in a wide set of settings, e.g. set-based simulation for hybrid systems, or floating point analysis, providing relational abstraction of functions with a cost linear in the number of errors terms. In this paper, we propose a quadratic version of zonotopes. We also present a new algorithm based on semi-definite programming to project a quadratic zonotope, and therefore quadratic forms, to intervals. All presented material has been implemented and applied on representative examples.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs

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 in which simple com putations update internal states and produce commands to update the system state. Those systems are yet hardly analyzable by available static analysis method, since, even if performing mainly linear computations, the computation of a safe set of reachable states often requires quadratic invariants. In this paper we consider the general setting of a piecewise affine program; that is a program performing different affine updates on the system depending on some conditions. This typically encompasses linear controllers with saturations or controllers with different behaviors and performances activated on some safety conditions. Our analysis is inspired by works performed a decade ago by Johansson et al, and Morari et al, in the control community. We adapted their method focused on the analysis of stability in continuous-time or discrete-time settings to fit the static analysis paradigm and the computation of invariants, that is over-approximation of reachable sets using piecewise quadratic Lyapunov functions.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Invariant stream generators using automatic abstract transformers based on a decidable logic

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 of the best approaches to discover useful invariants, especially numerical ones. However, its application is limited by two orthogonal issues: (i) developing an abstract interpretation is often non-trivial; each transfer function of the system has to be represented at the abstract level, depending on the abstract domain used; (ii) with precise but costly abstract domains, the information computed by the abstract interpreter can be used only once a post fix point has been reached; something that may take a long time for very large system analysis or with delayed widening to improve precision. This paper proposes a new, completely automatic, method to build abstract interpreters. One of its nice features is that its produced interpreters can provide sound invariants of the analyzed system before reaching the end of the post fix point computation, and so act as on-the-fly invariant generators.

0 citations0 reviewsNo code linkedOpen access