Kangfeng (Randall) Ye
Kangfeng (Randall) Ye
Home
Publications
News
Talks
Posts
Projects
Teaching
Showcases
Contact
Light
Dark
Automatic
Theorem Proving
Formally verified animation for RoboChart using interaction trees
RoboChart is a core notation in the RoboStar framework. It is a timed and probabilistic domain-specific and state machine-based …
Kangfeng Ye
,
Simon Foster
,
Jim Woodcock
Cite
DOI
URL
Probabilistic relations for modelling epistemic and aleatoric uncertainties: its semantics and automated reasoning with theorem proving
A RoboStar seminar: a summary of our recent work in modelling and verification of probabilistic programs.
Jun 28, 2023
PDF
Project
Project
Formally Verified Animation for RoboChart Using Interaction Trees
A RoboStar seminar: preparation and rehearsal for a presentation given later in ICFEM 2022
Oct 19, 2022
Project
Project
Probabilistic modelling and verification using RoboChart and PRISM
A RoboStar seminar: preparation and rehearsal for a presentation given later in MODELS 2022
Oct 5, 2022
Project
The submission (Formally Verified Animation for RoboChart using Interaction Trees) to ICFEM2022 is accepted
Jun 27, 2022
CyPhyAssure (June 2021 - August 2021)
CyPhyAssure
is a EPSRC funded project. It is also a
RoboStar
project.
Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving @ RAMiCS2021
Presentation for RAMiCS2021
Nov 4, 2021
PDF
Project
Slides
Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving
Rehearsal for RAMiCS2021 on 4th November, 2021
Oct 29, 2021
Project
Animation of RoboChart with Interaction Trees
Animation of RoboChart using Interaction Trees based CSP and code generation in Isabelle
Oct 6, 2021
Project
Isabelle/UTP Tutorial in Chinese
A Isabelle/UTP tutorial to the students in the computer science in Southwest University during three-days’ workshop. The tutorial is about 1 day (two afternoon).
May 13, 2019
Cite
×
