Deductive verification of stochastic hybrid systems with Isabelle/HOL

Stochastic hybrid systems are increasingly used to model safety-critical applications in robotics and autonomous systems, where uncertainty arises from sensor noise, actuator errors, and unpredictable environments. Ensuring the safety of these systems requires rigorous formal guarantees, yet existing verification tools often struggle with the combined complexity of continuous, discrete, and stochastic behavior.

In this thesis, we introduce a framework for the deductive verification of stochastic hybrid systems (SHS). This is centered around the Isabelle/HOL implementation of stochastic differential dynamic logic (SdL), a logic which allows for the verification of SHS by modelling them as stochastic hybrid programs (SHP). To complement our SdL implementation, we develop the foundational mathematical theories for defining and reasoning about continuous-time stochastic processes. We also present a simulation tool for SHPs, which aids the verification effort by enabling the validation of models before verification is attempted.