Certifying optimality of state estimation programs

Grigore Roşu, Ram Prasad Venkatesan, Jon Whittle, Laurenţiu Leuştean

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

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.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsWarren A. Hunt, Fabio Somenzi
PublisherSpringer-Verlag Berlin Heidelberg
Pages301-314
Number of pages14
ISBN (Print)3540405240, 9783540405245
DOIs
StatePublished - 2003

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2725
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Certifying optimality of state estimation programs'. Together they form a unique fingerprint.

  • Cite this

    Roşu, G., Venkatesan, R. P., Whittle, J., & Leuştean, L. (2003). Certifying optimality of state estimation programs. In W. A. Hunt, & F. Somenzi (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 301-314). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2725). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-540-45069-6_30