Our journal submission: Formally verified animation for RoboChart using interaction trees, was accepted and available online Dec 29, 2023 The paper is available here. 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.