formal verification

Invariant generation is crucial to the success of rigorous deductive verification tools for cyber-physical system. We develop a dedicated invariant generation toolbox for the KeYmaera X theorem prover which combines many custom invariant generation methods under a unified framework. Additionally, we develop a generalization of the method of barrier certificates (vector barrier certificates), building on R. Bellman's work on vector Lyapunov functions.

During the development process of CPS, an analysis of whether the system operates safely in its target environment is of utmost importance. For many applications of CPS research such as the transportation industry, this implies interconnected research in formal verification of CPS with research on knowledge representation and reasoning in multi-agent systems. The need for such research has become tragically clear in transportation accidents, one notorious case being the Air France 447 flight incident.