4 citations · 6 across the 8 of their papers we have counts for
8 papers
FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection
Julien Bortolussi, Dorra Ben Khalifa, Pierre-Loïc Garoche
Writing error-free floating-point programs is a challenging task, especially for programmers who lack a strong background in numerical analysis and rounding-error propagation. Stat…
Teaching Synchronous Dataflow Modelling with Learn-Heptagon
Pierre-Loïc Garoche, Basile Pesin
Lustre is a synchronous dataflow language designed to implement safety-critical embedded software. In addition to writing executable programs, the language doubles as a program log…
Quadratic Characterizations for Reachability Analysis of Neural Networks
Elias Khalife, Mazen Farhood, Pierre-Loic Garoche
Quadratic constraints (QCs) are widely used to characterize nonlinearities and uncertainties, but generic analytical characterizations can be conservative on bounded domains. This…
Formally Proving Invariant Systemic Properties of Control Programs Using Ghost Code and Integral Quadratic Constraints
Elias Khalife, Pierre-Loic Garoche, Mazen Farhood
This paper focuses on formally verifying invariant properties of control programs both at the model and code levels. The physical process is described by an uncertain discrete-time…
Optimization with Temporal and Logical Specifications via Generalized Mean-based Smooth Robustness Measures
Samet Uzun, Purnanand Elango, Pierre-Loic Garoche +1
This paper introduces a generalized mean-based C^1-smooth robustness measure over discrete-time signals (D-GMSR) for signal temporal logic (STL) specifications. In conjunction with…
Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers
Céline Bellanger, Pierre-Loïc Garoche, Matthieu Martel +1
Signal Temporal Logic (STL) is a convenient formalism to express bounded horizon properties of autonomous critical systems. STL extends LTL to real-valued signals and associates a…
Set-based value operators for non-stationary Markovian environments
Sarah H. Q. Li, Assalé Adjé, Pierre-Loïc Garoche +1
This paper analyzes finite state Markov Decision Processes (MDPs) with uncertain parameters in compact sets and re-examines results from robust MDP via set-based fixed point theory…
Credible Autocoding of Convex Optimization Algorithms
Timothy Wang, Romain Jobredeaux, Marc Pantel +3
The efficiency of modern optimization methods, coupled with increasing computational resources, has led to the possibility of real-time optimization algorithms acting in safety cri…