Abstract: “With the increasing power of computers, real-time algorithms tends to become more complex and therefore require better guarantees of safety. Among algorithms sustaining autonomous embedded systems, model predictive control (MPC) is now used to compute online trajectories, for example in the SpaceX rocket landing. The core components of these algorithms, such as the convex optimization function, will then have to be certified at some point. This paper focuses specifically on that problem and presents a method to formally prove a primal linear programming implementation.
We explain how to write and annotate the code with Hoare triples in a way that eases their automatic proof. The proof process itself is performed with the WP-plugin of Frama-C and only relies on SMT solvers. Combined with a framework producing all together both the embedded code and its annotations, this work would permit to certify advanced autonomous functions relying on online optimization.”
The neat thing about this work is the section on how they went about specifying and coding to get total automation. The main drawbacks of it are their heavily axiomatic approach that can lead to false proofs of correctness or that they delayed floating point for later. Assurance in the former can be increased by using theorems and axioms well-tested in practice. Also, deriving them from standard forms like set theory with checking by like Mizar or Isabelle/ZF. The floating point might be easier now with recent research automating it.