ProVE-Lab
ProVE ≡ ProVE, Validate, Execute
Formal verification plays a crucial role in making cyber-physical systems safe with strong guarantees about the system under a model of the system's behavior and its interaction with the environment. In cyber-physical systems, runtime safety is challenging because it requires predictions about physical dynamics in order to act ahead of time, before physics makes violating the desired safety properties inevitable. Building and verifying formal predictive models of intertwined computational and physical behavior, however, becomes increasingly difficult, since systems operate (semi-)autonomously and often utilize poorly understood learning-enabled components in unconstrained operating environments. This poses the double challenge of validating formal models from observations while simultaneously providing safety guarantees about unverified learned components and the true runtime behavior.
The PROVE-Lab researches logical foundations and tools for theorem proving, verified runtime monitoring, model validation, code synthesis, and safe learning. Together, these techniques provide true runtime safety guarantees by transferring proofs about models of cyber-physical systems to their actual runtime behavior.
