Certifying optimality of state estimation programs

The theme of this paper is certifying software for state estimation of dynamic systems, which is an important problem found in spacecraft, aircraft, geophysical, and in many other applications. The common way to solve state estimation problems is to use Kalman filters, i.e., stochastic, recursive algorithms providing statistically optimal state estimates based on noisy sensor measurements. We present an optimality certifier for Kalman filter programs, which is a system taking a program claiming to implement a given formally specified Kalman filter, as well as a formal certificate in the form of assertions and proof scripts merged within the program via annotations, and tells whether the code correctly implements the specified state estimation problem. Kalman filter specifications and certificates can be either produced manually by expert users or can be generated automatically: we also present our first steps in merging our certifying technology with AUTOFILTER, a NASA Ames state estimation program synthesis system, the idea being that AUTOFILTER synthesizes proof certificates together with the code.