4 papers
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…