formal verification


Visible to the public Sound Invariant Generation for Continuous and Hybrid Systems

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.


Visible to the public Belief-Aware Cyber-Physical Systems

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.