34 citations · 119 across the 18 of their papers we have counts for
8 papers · 1 filter
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…
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…
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…