Ph.D. Defense: Raphael Cohen

Mon Dec 03 2018 11:00 AM to 01:00 PM
TSRB (Tech Square) Room 509
“Formal Verification and Validation of Convex Optimization Algorithms for Model Predictive Control”

You're invited to attend

Ph.D. Defense

by

Raphael Cohen

(Advisor: Prof. Eric Feron)

“Formal Verification and Validation of Convex Optimization Algorithms for Model Predictive Control”

on
 

Monday, December 3 at 11 a.m.
TSRB (Tech Square) Room 509

Abstract:
The efficiency of modern optimization methods, coupled with increasing computational resources, has led to the possibility of real-time optimization algorithms acting in safety critical roles. However, this cannot happen without addressing proper attention to the soundness of these algorithms. This PhD thesis discusses the formal verification of convex optimization algorithms with a particular emphasis on receding-horizon controllers. Additionally, we demonstrate how theoretical proofs of real-time optimization algorithms can be used to describe functional properties at the code level, thereby making it accessible for the formal methods community. In seeking zero-bug software, we use the Credible Autocoding scheme. We focused our attention on the ellipsoid algorithm solving second-order cone programs (SOCP). In addition to this, we present a floating-point analysis of the algorithm and give a framework to numerically validate the method.

Committee:

  • Professor Marcus Holzinger, Georgia Tech / Univ. Colorado Boulder
  • Professor Panagiotis Tsiotras, Georgia Tech
  • Professor Eric Feron, Georgia Tech
  • Dr. Pierre-Loïc Garoche, Onera - The French Aerospace Lab
  • Dr. Tim Wang, UTRC
  • Dr. César Muñoz, NASA

Location

TSRB (Tech Square) Room 509