Using semidefinite programming to find invariants for automatic reasoning tools

Abstract:

An important and dificult problem in engineering is the automatic verification of complex and safety critical systems. Much research eort 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 suffer 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 suffer 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 differential equations, which involve transcendental functions even for linear differential 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.