Proof carrying code generation of embedded optimization programs

Optimization algorithms are now seriously considered to be embedded as part of the most critical systems. Potential applications range from engine control, trajectory computation, or aircraft control. Efficient convex optimization algorithms are now available thanks to the existence of interior point methods. However to be able to embed such algorithms in real-time system, for example in future aircraft, one need to be able to show that these algorithms will perform as expected: computing a feasible optimal solution in a given time. This work presents our approach and early results towards the certification of optimization algorithms. This is a joint work with Guillaume Davy, Eric Feron, and Didier Henrion