Kangfeng Ye

Research Associate (Computer Science)

University of York


I am a research associate in the Circus group, which is a part of the Department of Computer Science at University of York. The group name Circus stands for Concurrent Integrated Refinement CalculUS, a formal language for specification and refinement.

I have a particular interest in applying mathematics and logic in software engineering. To be more specific, it is application of formal specification and verification in safety critical systems, cyber physical systems (CPS) and robotics. My interests lie in several aspects:

  • formal specification using Z, CSP or Circus;
  • denotational and operational semantics using Unifying Theories of Programming (UTP);
  • formal verification using model checking and theorem proving (Isabelle);
  • tool development to assist application of formal methods.


  • Model-based design and test
  • Cyber Physical Systems and Robotics
  • Formal methods (UTP, CSP, Z, Circus, …)
  • Formal verification
  • Uncertainty modelling (probability theory and verification).


  • PhD in Computer Science, 2016

    University of York



RoboSoft is a two-day event to bring together researchers representing groups working on themes relevant for Software Engineering for …

Second visit of Prof. Zhiming Liu's team at York

very glad to meet Prof. Zhiming Liu’s team again at York

Visit of Prof. Zhiming Liu's team at York

Very very glad to meet Prof. Zhiming Liu’s team from Southwest University (SWU)

RoboTest RoboCalc Advisory Board meeting

Recent Posts

Belief-Desire-Intention (BDI)

BDI is new to me and better to know a bit about it.

Testing Robotic Systems

A talk by Arnaud Gotlieb in RoboSoft

Evolving Robot Software and Hardware

A talk by Prof. Gusz Eiben in RoboSoft


Engineering Line Following Robot

The map shown on the right is a Formula One circuit: Brands_Hatch that I use to run my LFR experience.


CSAV2018 - Teaching Assistant

As a TA, I got positive feedback from students regarding my contribution in the practical courses.


RoboCalc (April 2018 - Present)

RoboCalc is a EPSRC funded project. It is also a RoboStar project.

INTO-CPS (Dec 2016 - Dec 2017)

INTO-CPS (Integrated Tool Chain for Model-based Design of Cyber-Physical Systems) is a EU Horizon 2020 project, from 2015 to 2017. …

Recent & Upcoming Talks

RoboChart & RoboTool: modelling and verification of probabilistic systems

A tutorial on how to use RoboChart and RoboTool to model and verify probabilistic systems.

Modelling and verification of probabilistic behaviour of robotic applications

This talk presents how our RoboTool uses PRISM to analyse probability properties of robotic applications by transforming RoboChart to …

Engineering Robotic Swarms

A pint of science talk by me, James Baxter and Richard Redpath from our group.

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 …

Recent Publications


  • Department of Computer Science, Deramore Lane, University of York, Heslington, York, CA, YO10 5GH, United Kingdom
  • CSE/011