*********************************
There is now a CONTENT FREEZE for Mercury while we switch to a new platform. It began on Friday, March 10 at 6pm and will end on Wednesday, March 15 at noon. No new content can be created during this time, but all material in the system as of the beginning of the freeze will be migrated to the new platform, including users and groups. Functionally the new site is identical to the old one. webteam@gatech.edu
*********************************
PhD Defense
Formal Verification and Validation of Convex
Optimization Algorithms For Model Predictive Control
Student Name: Raphael Cohen
Advisor: Dr. Eric Feron
Date and time: December 3rd 2018 in TSRB (Tech square) room 509 at 11 am
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.
keywords: Formal Methods, Software Verification, Frama-C, SMT Solvers, Convex Optimization, Ellipsoid Method, Floating-points.
Committee Member:
