Breakthrough in the testing of cyber-physical systems

In the world of formal logic and mathematical models used for cyber-physical systems and the planning of robot movements, certain statements are very important. These statements use the words "there is" and "for all". However, they are difficult for humans and computers to understand when it comes to cyber-physical systems, and not just statements like "there is a real number whose square is 5" or "all real numbers have non-negative squares". The best way to analyze these statements is a process called quantifier elimination (QE). QE converts these complicated statements into simpler but equivalent formulas that do not use the words "there is" and "for all". These simpler formulas can be easily evaluated.

It is crucial for the security of cyber-physical systems that the QE algorithms function correctly. To ensure this, the algorithms can be implemented in a theorem prover and their correctness can be proven mathematically. These proofs are very accurate because they rely only on a small and trustworthy core of the program.

In her dissertation "Formal verification of quantifier elimination algorithms" under the supervision of Prof. André Platzer, Katherine Kosaian focused on this problem. Kosaian formalizes virtual substitution as an incomplete but practically relevant quantifier elimination technique and provides verified algorithms via code generation that are experimentally competitive with non-verified state-of-the-art algorithms, but provably correct. In addition to virtual substitution, the thesis also covers complete quantifier elimination algorithms. In particular, it provides the first algorithm for complete setting with formulas and quantifiers of multivariate polynomials that is formally verified in Isabelle/HOL.

"Katherine Kosaian's work is a significant advance in formal verification and provides new tools and methods that help to develop safer and more reliable cyber-physical systems and robot motion planning," explains Professor Platzer. For her theoretical and practical contributions to formally verified quantifier elimination, the scientist received the prestigious Bill McCune PhD Award 2024 at the 12th International Conference on Automated Deduction (CADE).

Award winner Katherine Kosaian with PhD supervisor André Platzer (left) and Carsten Fuhs (Image: Jürgen Giesl)

Katherine Kosaian completed her doctorate with Prof. André Platzer at Carnegie Mellon University until 2023 and is now starting as an assistant professor at the University of Iowa after a postdoctoral year at Iowa State University. Platzer holds the Alexander von Humboldt Professorship for Logic of Autonomous Dynamical Systems at the Karlsruhe Institute of Technology and is the founder of the Logical Systems Lab at Carnegie Mellon University. In his research, he focuses on the development and application of differential dynamic logics and has made a decisive contribution to the safety testing of cyber-physical systems in areas such as transportation, aviation, shipping and robotics.