TY - JOUR
T1 - Formal Verification for Embedded Implementation of Convex Optimization Algorithms
AU - Cohen, Raphael
AU - Davy, Guillaume
AU - Feron, Eric
AU - Garoche, Pierre Loïc
N1 - Generated from Scopus record by KAUST IRTS on 2021-02-18
PY - 2017/7/1
Y1 - 2017/7/1
N2 - 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.
AB - 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.
UR - https://linkinghub.elsevier.com/retrieve/pii/S2405896317318219
UR - http://www.scopus.com/inward/record.url?scp=85031796587&partnerID=8YFLogxK
U2 - 10.1016/j.ifacol.2017.08.1300
DO - 10.1016/j.ifacol.2017.08.1300
M3 - Article
SN - 2405-8963
VL - 50
SP - 5867
EP - 5874
JO - IFAC-PapersOnLine
JF - IFAC-PapersOnLine
IS - 1
ER -