Formal Verification for Embedded Implementation of Convex Optimization Algorithms

Raphael Cohen (1, 2) , Guillaume Davy (3, 2) , Eric Féron (1) , Pierre-Loïc Garoche (2)

1 Georgia Institute of Technology [Atlanta]
2 ONERA - The French Aerospace Lab [Toulouse]
3 LAAS-MAC - Équipe Méthodes et Algorithmes en Commande

Advanced embedded algorithms are growing in complexity and length, related to the growth in autonomy, which allows systems to plan paths of their own. However, this promise cannot happen without proper attention to the considerably stronger operational constraints that safety-critical applications must meet. This paper discusses the formal verification for optimization algorithms with a particular emphasis on receding-horizon controllers. Following a brief historical overview, a prototype autocoder for embedded convex optimization algorithms will be discussed. Options for encoding code properties and proofs, and their applicability and limitations will be detailed as well.

Mots clés: FORMELLE; VERIFICATION; CONVEXE

Domaines: Algorithme et structure de données [cs.DS]

Raphael Cohen, Guillaume Davy, Eric Féron, Pierre-Loïc Garoche. Formal Verification for Embedded Implementation of Convex Optimization Algorithms. IFAC-PapersOnLine, 2017, 50 (1), pp.5867-5874. ⟨10.1016/j.ifacol.2017.08.1300⟩. ⟨hal-01850596⟩