From Lustre to Simulink: reverse compilation for embedded systems applications

Parabolic set simulation for reachability analysis of linear time-invariant systems with integral quadratic constraint

This paper describes the computation of reachable sets and tubes for linear time-invariant systems with an unknown input bounded by integral quadratic constraints, modeling e.g. delay, rate limiter, or energy bounds. We define a family of …

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 …

Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems

A Sums-of-Squares Extension of Policy Iterations

Automatic synthesis of k-inductive piecewise quadratic invariants for switched affine control programs

Abstract Among the various critical systems that are worth to be formally analyzed, a wide set consists of controllers for dynamical systems. Those programs typically execute an infinite loop in which simple computations update internal states and …

Credible Autocoding of Convex Optimization Algorithms

Practical Policy Iterations A practical use of policy iterations for static analysis - The quadratic case.

Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses

Formal Verification of Critical Aerospace Software