1

Semidefinite Approximations of Reachability Sets for Discrete-time Polynomial Systems

Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs

Certificate-carrying modular compilation

Closed Loop Analysis of Control Command Software

Compilation Of Synchronous Observers As Code Contracts

Credible autocoding of convex optimization algorithms

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

Property-based polynomial invariant generation using sums-of-squares optimization

Quadratic Zonotopes - An Extension of Zonotopes to Quadratic Arithmetics

Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison