1

Ensuring functional correctness of cyber-physical system controllers: from model to code analyses

Automatic Generation and Formal Verification of an Interior Point Method Algorithm

Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm

Automated analysis of Stateflow models

Formal Verification for Embedded Implementation of Convex Optimization Algorithms

Semi-Definite Programs for Discrete-time Piecewise Affine Systems

Semidefinite Approximations of Reachable Sets for Discrete-Time Polynomial Systems

Validation of Convex Optimization Algorithms and Credible Implementation for Model Predictive Control

Formal Analysis of Robustness at Model and Code Level

Hierarchical State Machines as Modular Horn Clauses