Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm

DOI10.29007/qt5jzbMath1415.68143arXiv1801.03833OpenAlexW2892600584MaRDI QIDQ5222962

Pierre-Loïc Garoche, Guillaume Davy, Eric Feron, Didier Henrion

Publication date: 4 July 2019

Published in: EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1801.03833

zbMATH Keywords

convex optimizationinterior-point methodprogram analysismodel predictive controlsatisfiability modulo theorynumerical software verification

Mathematics Subject Classification ID

Interior-point methods (90C51) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

A constraint-separation principle in model predictive control

Uses Software

• ACSL
• CVX
• Frama-C

This page was built for publication: Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm