Probabilistic modelling and verification using RoboChart and PRISM Oct 5, 2022 Project RoboChart Verification Theorem Proving Isabelle Probabilistic UTP Formal semantics Mechanisation Kangfeng (Randall) Ye Research Associate (Computer Science) My research interests include probabilistic modelling and verification using formal specification and verification (both model checking and theorem proving) and model-based engineering.