Biological applications of hybrid systems verification

We show how techniques developed for formal verification of hybrid systems can be applied to biological examples. Hybrid systems are mathematical models that combine discrete and continuous behaviour. They have been traditionally used for modelling and analysing cyber-physical systems, which feature digital computing cores interacting with a physical environment (e.g., infusion pumps, cruise control, etc.) Recently, hybrid systems have found application in biological contexts for modelling complex systems involving discrete modes and continuous behaviour. In this talk we focus on hybrid models of cardiac cells and of prostate cancer therapies. In particular, we use delta-complete verification techniques to identify parameter ranges related to cardiac disorders and to predict patient-specific prostate cancer therapies.