Skip to content

index.md

Latest commit

 

History

History
398 lines (278 loc) · 31.5 KB

index.md

File metadata and controls

398 lines (278 loc) · 31.5 KB

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

Kangfeng Ye (also known as Randall Ye)

<style> img[src*="#round"]{ border-radius: 50%; } img[src*="#middle"] { width:450px; } img[src*="#small"] { width:200px; } </style>
Kangfeng Ye

I left the University of York in November 2025 and joined IOHK as a formal methods engineer.

Short background

Since Nov 2025: Industry at IOHK

: Formal methods engineer

2016 - 2025: 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 probabilistic verification for robotic applications, and a contributor 1 of Isabelle/UTP, a unifying semantic framework supporting theorem proving. Both tools are being developed in the RoboStar group.

2012 - 2016: PhD at the University of York (Formal methods)

: Supervised by Prof. Jim Woodcock. The most right choice in my career is to have a PhD in formal methods with Jim. Every time when I think of him, I always feel 🙂 ☀️ and calm and passionate 🔥 in research because of the knowledge he taught me and the way being a good researcher.

: 📚 Thesis: Model Checking of State-Rich Formalisms (By Linking to Combination of State-based Formalism and Process Algebra)

2004 - 2012: Industry (Embedded Software Engineer/Lead) : 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

🔑 Formal verification 🔑 Formal semantics 🔑 Probabilistic programming languages 🔑 Probabilistic model checking 🔑 Probabilistic theorem proving 🔑 Model-based Software Engineering 🔑 Cyber-Physical Systems 🔑 Cryptographic security protocols 🔑 Tool development

Research interests and summary

Probabilistic programming: semantics and verification

➡️ Probabilistic semantics and verification for RoboChart using PRISM

➡️ Probabilistic Unifying Relations (ProbURel)

➡️ Probabilistic designs

➡️ Quantitative Analysis of UML Activity Diagrams

➡️ QoS (energy efficiency and service availability) analysis of O-RAN xApps

Formal specification languages

Z notation and Circus

➡️ Model checking of Circus

➡️ An ISO Z and Circus Parser and Typechecker

  • 🔆 A complete implementation2 of ISO Z Standard (ISO/IEC 13568:2002) 🔆 Most Circus Syntax
  • 📚: Haven't published yet 🙁
  • 🛠️: ISOZ and Circus Parser and TypeChecker, implemented using Alex and Happy in Haskell, also C++.
  • 📒 Examples from the standard documentation, Circus buffer, reactive buffer, Circus steam boiler

➡️ Reactive Relations3

CSP

➡️ Animation of RoboChart

Graphical Notations

➡️ Assume-Guarantee Reasoning of Simulink

➡️ Probabilistic semantics and animation for the state-machine based RoboChart (see details above)

UVC Human State Machine

➡️ Quantitative Analysis of UML Activity Diagrams (see details above)

PAL use case

Formal verification of security protocols

➡️ Formal verification of security protocols using animation, a lightweight model checker

Member of Groups

News

General

2025-11-24 New journey in industry at IOHK : I joined IOHK as a formal methods engineer.

2025-11-21 Last day at the University of York : I left the UoY after 13 years there (4 years as PhD and 9 years as RA).

2025-11-13 My first submission (Abel's Limit Theorem) to Isabelle AFP (Archive of Formal Proofs) was accepted : While Abel's limit theorem in mathematical analysis was mechanised in Lean, but not yet in Isabelle. This entry mechanises Abel's limit theorem on power series with real coefficients in Isabelle.

Papers

2025-11-11 ICFEM2025 paper availabel online at Springer : Now our paper (Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks) is available online.

2025-08-02 Paper accepted by ICFEM2025 : Our paper, titled "Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks", submitted to ICFEM2025 was accepted.

2025-04-18 DataMod24 paper available online : Towards Achieving Energy Efficiency and Service Availability in O-RAN via Formal Verification from Springer

2025-01-16 Interviewed by Dr. Daniel Shea on Scholarly Communication : I was interviewed on Scholarly Communication by Dr. Daniel Shea from Karlsruhe Institute of Technology (KIT) for one of my co-authored paper: Probabilistic Modelling and Verification Using RoboChart and PRISM. The paper was published in the journal of Software and Systems Modeling and won the Journal-First award. I was invited to present the paper at MODELS 2022. The episode is now available here.

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)

2025-07-15 to 2025-07-16: CHEDDAR and 'Friends' Symposium and Industry Days, London : I presented the select CHEDDAR highlight project 3.2 (formal verification) from the University of York (collaborated with the University of Glasgow and Imperial College London). My slides are available here.

2025-03-03 to 2025-03-06: MWC2025 at Barcelona, Spain : A Linkedin post about our demo "User-Guided Verification of Security Protocols via Sound Animation", also a video available at Youtube.

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

Awards

2022 SoSyM Journal-first : For the paper Probabilistic Modelling and Verification Using RoboChart and PRISM SoSyM Journal-first

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,\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. [==PLS==] K. Ye, R. Metere, J. Woodcock, and P. Yadav, “Formal verification of physical layer security protocols for next-generation communication networks,” in Formal Methods and Software Engineering, É. André, J. Wang, and N. Zhan, Eds., Singapore: Springer Nature Singapore, 2026, pp. 1–21, isbn: 978-981-95-4213-0. � doi: 10.1007/978-981-95-4213-0_1.

  2. [==Sound animation==] K. Ye, R. Metere, and P. Yadav, “User-Guided Verification of Security Protocols via Sound Animation,” in Software Engineering and Formal Methods (SEFM), Springer Nature Switzerland, Nov. 2024, pp. 33–51, isbn: 9783031773822. � doi: 10.1007/978-3-031-77382-2_3.

  3. [==O-RAN xApp==] R. Metere, K. Ye, Y. Gu, et al., “Towards Achieving Energy Efficiency and Service Availability in O-RAN via Formal Verification,” in From Data to Models and Back (DataMod2024), Springer International Publishing, 2024. � doi: 10.1007/978-3-031-87908-1_9.

  4. [==Probabilisic case study==] 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.

  5. [==RoboChart Animation==] 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.

  6. [==Probabilistic Theorem Provering==] 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.

  7. [==Probabilistic Semantics==] 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.

  8. [==Reactive relations==] 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.

Formal proofs (published)

  1. K. Ye, “Abel’s limit theorem,” Archive of Formal Proofs, Nov. 2025, https://isa-afp.org/entries/Abel_Limit_Theorem.html, Formal proof development, issn: 2150-914x.

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 CHEDDAR and 'Friends' Symposium and Industry Days - 15/16 July, London : I presented the select CHEDDAR highlight project 3.2 (formal verification) from the University of York (collaborated with the University of Glasgow and Imperial College London). My slides are available here.

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 (I was or am working on)

CHEDDAR (Feb 2024 - Nov 2025) : The Communications Hub for Empowering Distributed Cloud Computing Applications and Research (CHEDDAR)

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-funded (Simon Foster's fellowship) project

Compositional Assume-Guarantee Reasoning of Control Law Diagrams using UTP (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 together

JWFS 2024 PC member : The Festschrift for Prof. Jim Woodcock on the occasion of his retirement from the University of York

Contact

Footnotes

  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. Except semantics transformation rules (a small part is implemented) ↩

  3. relatively small contribution to this work, mainly in the verificaiton of the reactive buffer, and gave Simon some insight on the verificaiton strategy when he was developing the theory. But this is very beautiful work and it is nice to mention here. ↩

  4. Circus members are now mostly in RoboStar ↩