Home | Short background | Research interests | News | Publications | Talks and Presentations |
Projects | Posts | Showcases | Academic activities | Contact

Kangfeng Ye (also known as Randall Ye)

Kangfeng Ye

I am a Research Associate at the University of York, working in the Department of Computer Science.

I am creating a simpler academic homepage and migrating contents from old entry.

▶︎
all
running...

Short background

2012 - now: Academia (Formal methods in robotics, probabilistic programming, and security)

In my research, I use mathematical logic (alphabetised predicate calculus in Unifying Theories of Programming - UTP) to give probabilistic semantics (denotational and operational semantics) to a domain-specific language (RoboChart) in robotics, with support of modelling time and probability, (2) develop automated verification tools using modern model-based techniques (model transformation, validation, and generation) and formal verification (model checking and theorem proving), and apply theoretical semantics and practical tools to a variety of case studies.

I am a developer of RoboTool supporting formal verification for robotic application, and a contributor [1] of Isabelle/UTP, a unifying semantic framework supporting theorem proving. Both tools are being developed in the RoboStar group.

2004 - 2012: Industry (Embedded Software Engineer)

Led a team (4-8 members) to develop embedded software for lithography, Ethernet Datacenter Switch, and Communication devices

C/C++, MCU, Linux, VxWorks

Research Keywords

Research interests

Probabilistic programming: semantics and verification

Formal verification of robotic software controllers

Formal verification of security protocols

Model-based software engineering

Member of Groups

News

Papers

2024-11-06 The preprint of the DataMod24 paper is available
The preprint of our paper "Towards Achieving Energy Efficiency and Service Availability in O-RAN via Formal Verification" can be found here.
2024-10-07 Paper accepted by DataMod24
Our paper submitted to DataMod24 has been accepted for publication. This paper is about the quantitative analysis of a control policy used in an O-RAN xApp to achieve energy efficiency and guarantee service availability. We use PRISM to verify a scenario with 3 radio cells (stations) and 9 UEs (user equipments) while UEs are dynamically and uncertainly switched on and off.
2024-10-01 The preprint of the SEFM2024 paper is available
The preprint of our paper "User-Guided Verification of Security Protocols via Sound Animation" can be found here. Please note that this is not the final camera ready version
2024-09-25
Our TCS journal paper (about probabilistic programming) is now online
2024-09-12
Our TCS journal paper (about probabilistic programming) has been accepted for publication and should be online soon.
The first draft is available online at arxiv
2024-09-01
A joint Festschrift paper, titled "A Tour Through the Programming Choices: Semantics and Applications", with Pedro Ribeiro, Frank Zeyda, and Alvaro Miyazawa to celebrate Prof. Jim Woodcock's retirement from York. He was my PhD supervisor and a line manager in RoboStar.
2024-08-22
Our paper (User-Guided Verification of Security Protocols via Sound Animation) submitted to SEFM24 has been accepted for publication.
2023-12-19
Our JLAMP journal paper (Formally verified animation for RoboChart using interaction trees) has been accepted for publication.

Events (I attended)

2024-11-06 to 2024-11-08: SEFM2024 at Aveiro, Portugal
I presented our work "User-Guided Verification of Security Protocols via Sound Animation" at SEFM2024. The slide is available here
2024-09-26 Cheddar All-hands meeting in Imperial
Presentations from new partners, demonstration discussion, and updates from each pillar. I have updated P3.2 from York regarding accessible formal techniques using sound animation and quantitative analysis of energy efficiency and service availability in O-RAN xApps (to optimise QoS).
2024-09-04 Jim's Festschrift
I have been greatly benefited from Jim’s inspiration and mentorship. I and Pedro presented our paper "A Tour Through the Programming Choices: Semantics and Applications". It's my pleasure to present Frank's preferential choice and my work ProbURel (collaborated with Jim and Simon) in probabilistic semantics and theorem proving.
2024-07-25 6G Summit in Leeds
Co-located with WINCOM2024
2024-07-09
Cheddar project meeting at the Cranfield University
2024-06-27
Gave a talk in the University's Celebrating Spaces: Connecting Researchers. It is a 5-minute Lightning Talk. My talk is about Guarantee correctness and performance of probabilistic algorithms.
2024-06-05 to 06
Cheddar Pillar 1 and P3.2 meetings at the University of Glasgow
2024-03-28
Cheddar P3.1 and P3.2 joint meeting at Imperial College London
2024-03-12
Cheddar Bi-Annual meeting at the University of York

Publications

Journal article

  1. [ProbURel] K. Ye, J. Woodcock, and S. Foster, “Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: Semantics and automated reasoning with theorem proving,” Theoretical Computer Science, p. 114 876, 2024, issn: 0304-3975.  doi: 10.1016/j.tcs.2024.114876.

  2. [RoboChart_ITrees] K. Ye, S. Foster, and J. Woodcock, “Formally verified animation for RoboChart using interaction trees,” Journal of Logical and Algebraic Methods in Programming, vol. 137, p. 100 940, 2024, issn: 2352-2208.  doi: 10.1016/j.jlamp.2023.100940.

  3. [RoboChart_PRISM] K. Ye, A. Cavalcanti, S. Foster, A. Miyazawa, and J. Woodcock, “Probabilistic modelling and verification using RoboChart and PRISM,” en, Software and Systems Modeling, vol. 21, no. 2, pp. 667–716, Apr. 2022, issn: 1619-1374.  doi: 10.1007/s10270-021-00916-8.

  4. [Reactive_Relations] S. Foster, K. Ye, A. Cavalcanti, and J. Woodcock, “Automated Verification of Reactive and Concurrent Programs by Calculation,” Journal of Logical and Algebraic Methods in Programming, vol. 121, p. 100 681, Jun. 2021, arXiv:2007.13529 [cs], issn: 23522208.  doi:
    10.1016/j.jlamp.2021.100681.

  5. [ModelChecking_Circus] K. Ye and J. Woodcock, “Model checking of state-rich formalism by linking to CSP ∥ BCSP\,\Vert \,B,” en, International Journal on Software Tools for Technology Transfer, vol. 19, no. 1, pp. 73–96, Feb. 2017, issn: 1433-2787.  doi: 10.1007/s10009-015-0402-1. (visited on 10/13/2023).

Conference Proceedings

  1. M. Adam, K. Ye, D. A. Anisi, A. Cavalcanti, J. Woodcock, and R. Morris, “Probabilistic Modelling and Safety Assurance of an Agriculture Robot Providing Light-Treatment,” in 2023 IEEE 19th International Conference on Automation Science and Engineering (CASE), ISSN: 2161-8089, Aug. 2023, pp. 1–7.  10.1109/CASE56687.2023.10260395.

  2. K. Ye, S. Foster, and J. Woodcock, “Formally Verified Animation for RoboChart Using Interaction Trees,” en, in Formal Methods and Software Engineering, A. Riesco and M. Zhang, Eds., ser. Lecture Notes in Computer Science, Cham: Springer International Publishing, 2022, pp. 404–420, isbn: 978-3-031-17244-1.  10.1007/978-3-031-17244-1_24.

  3. K. Ye, S. Foster, and J. Woodcock, “Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving,” en, in Relational and Algebraic Methods in Computer Science, U. Fahrenberg, M. Gehrke, L. Santocanale, and M. Winter, Eds., ser. Lecture Notes in Computer Science, Cham: Springer International Publishing, 2021, pp. 465–482, isbn: 978-3-030-88701-8.  10.1007/978-3-030-88701-8_28.

  4. J. Woodcock, A. Cavalcanti, S. Foster, A. Mota, and K. Ye, “Probabilistic Semantics for RoboChart,” en, in Unifying Theories of Programming, P. Ribeiro and A. Sampaio, Eds., ser. Lecture Notes in Computer Science, Cham: Springer International Publishing, 2019, pp. 80–105, isbn: 978-3-030-31038-7.  10.1007/978-3-030-31038-7_5.

  5. S. Foster, K. Ye, A. Cavalcanti, and J. Woodcock, “Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra,” en, in Relational and Algebraic Methods in Computer Science, J. Desharnais, W. Guttmann, and S. Joosten, Eds., ser. Lecture Notes in Computer Science, Cham: Springer International Publishing, 2018, pp. 205–224, isbn: 978-3-030-02149-8.  10.1007/978-3-030-02149-8_13.

Books and Chapters

  1. P. Ribeiro, K. Ye, F. Zeyda, and A. Miyazawa, “A tour through the programming choices: Semantics and applications,” in The Application of Formal Methods. Springer Nature Switzerland, 2024, pp. 261–305, isbn: 9783031671142.  10.1007/978-3-031-67114-2_11.

  2. J. Woodcock, S. Foster, A. Mota, and K. Ye, “RoboStar Technology: Modelling Uncertainty in RoboChart Using Probability,” en, in Software Engineering for Robotics, A. Cavalcanti, B. Dongol, R. Hierons, J. Timmis, and J. Woodcock, Eds., Cham: Springer International Publishing, 2021, pp. 413–465, isbn: 978-3-030-66494-7.  doi: 10.1007/978-3-030-66494-7_13.

  3. K. Ye, S. Foster, and J. Woodcock, “Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP,” en, in From Astrophysics to Unconventional Computation: Essays Presented to Susan Stepney on the Occasion of her 60th Birthday, ser. Emergence, Complexity and Computation, A. Adamatzky and V. Kendon, Eds., Cham: Springer International Publishing,
    2020, pp. 215–254, isbn: 978-3-030-15792-0.  doi: 10.1007/978-3-030-15792-0_10.

PhD Thesis

  1. K. Ye, “Model Checking of State-Rich Formalisms (By Linking to Combination of State-based Formalism and Process Algebra),” en, phd, University of York, Aug. 2016.  url: https://etheses.whiterose.ac.uk/15526/.

Preprints

  1. K. Ye and J. Woodcock, RoboCertProb: Property Specification for Probabilistic RoboChart Models, 2024. arXiv: 2403.08136 [cs.LO].

  2. K. Ye, F. Yan, and S. Gerasimou, Quantitative Assurance and Synthesis of Controllers from Activity Diagrams, 2024. arXiv: 2403.00169 [cs.LO].

Talks and Presentations

Probabilistic programming

Lightning Talk on 2024-06-27
A 5-minute Lightning Talk, given at the University's Celebrating Spaces: Connecting Researchers. The talk video is now available at Youtube. My talk is about Guarantee correctness and performance of probabilistic algorithms.
Monkey in front of a cliff

Verification of security protocols

Presentation at SEFM2024 on the 7th of November, 2024
I presented our paper "User-Guided Verification of Security Protocols via Sound Animation" at SEFM2024. In this work, we address the accessibility of formal verification of security protocols for designers and the soundness guarantee of automatically generated animators. The slide is available here. More details can be found this post.

Projects

CHEDDAR (Feb 2024 - )
The Communications Hub for Empowering Distributed Cloud Computing Applications and Research [(CHEDDAR)}(https://cheddarhub.org/)
SESAME (June 2023 - Jan 2024)
Secure and Safe Multi-Robot Systems
RoboCalc and RoboTest (April 2018 - June 2023)
EPSRC projects in the RoboStar group
CyphyAssure (June 2021 - September 2021)
A EPSRC (Simon Foster's fellowship) project
VETSS (Oct 2017 - March 2018)
A VETSS sponsored project
INTO-CPS (Nov 2016 - Dec 2017)
Integrated Tool Chain for Model-based Design of Cyber-Physical Systems

Posts

2024-11-06 to 08
Application of formal verification in security protocols and O-RAN xApps

Showcases

Academic activities

Organiser of WINCOM2024 Hackathon and Demo
Organised with Ashan Khan
JWFS 2024 PC member
The Festschrift for Prof. Jim Woodcock on the occasion of his retirement from the University of York

Contact

  1. I made a few contributions to Isabelle/UTP, particularly in reactive designs and interaction trees. But in general, I am a user of Isabelle/UTP, and not a developer. ↩︎

  2. Circus members are now mostly in RoboStar ↩︎