Using semidefinite programming to find invariants for automatic reasoning tools

Nikos Aréchiga, CMU - Toyota


An important and dificult problem in engineering is the automatic veri fication of complex and safety critical systems. Much research e ort has been devoted to this problem, and the existing techniques can roughly be grouped into two categories: state-space exploration techniques and deductive techniques.

State-space exploration techniques try to show that a certain set of system states are not reachable by explicitly computing an overapproximation of the reachable state set. These techniques enjoy a high degree of automation, but often su ffer from artifacts due to linearization and other approximation errors.

Deductive techniques use automated reasoning tools such as theorem provers to construct a symbolic proof of system safety. In principle, this symbolic approach does not suff er from approximation errors, but state-of- the-art theorem provers require heavy interaction with a human user to guide the proof process.

One way to improve the performance of theorem provers is to improve their ability to find invariants for continuous and hybrid dynamics. Invariants allow the prover to sidestep the complex arithmetic that results from the solutions of diff erential equations, which involve transcendental functions even for linear di fferential equations, and often cannot be solved by arithmetic algorithms such as Tarski-Seidenberg quanti er elimination.

We discuss ongoing work to leverage techniques for invariant generation from traditional control theory to improve performance and degree of automation for the theorem proving tool KeYmaera.