- 2022-2023, Spring, Principles of Programming Languages, Graduate
- 2022-2023, Spring, Scientific Writing, Graduate
- 2022-2023, Autumn, Techniques and Methods for Programming, Undergraduate
- 2021-2022, Spring, Data Structures and Algorithms (in Python), Undergraduate
- 2021-2022, Spring, Scientific Writing, Graduate
- 2021-2022, Autumn, Techniques and Methods for Programming, Undergraduate
- 2020-2021, Spring, Techniques and Methods for Programming, Undergraduate
- 2020-2021, Spring, Scientific Writing, Graduate
- 2020-2021, Autumn, Data Structure (in Python), Undergraduate
- 2019-2020, Spring, Techniques and Methods for Programming, Undergraduate
- 2019-2020, Spring, Scientific Writing, Graduate
- 2019-2020, Autumn, Data Structure (in Python), Undergraduate
- 2018-2019, Spring, Techniques and Methods for Programming, Undergraduate
- 2018-2019, Autumn, Data Structure (in Python), Undergraduate
- 2017-2018, Spring, Software Formal Methods, Graduate
- 2017-2018, Autumn, Data Structure (in C), Undergraduate
- 2016-2017, Spring, Software Formal Methods, Graduate
- 2016-2017, Autumn, Data Structure (in Python), Undergraduate
- 2015-2016, Spring, Software Formal Methods, Graduate
- 2015-2016, Autumn, Data Structure (in Python), Undergraduate
- 2014-2015, Autumn, Data Structure (in C), Undergraduate
- 2013-2014, Autumn, Data Structure (in C), Undergraduate
- 2012-2013, Spring, Set Theory and Graph Theory, Undergraduate
- 2012-2013, Autumn, Data Structure (in C), Undergraduate
- 2011-2012, Spring, Selected Topics on Software Theory and Methodology (Model Checking), Graduate
- 2011-2012, Autumn, Data Structure (in C), Undergraduate
- 2010-2011, Spring, Selected Topics on Software Theory and Methodology (Algebraic Specification and Coalgebra Theory), Graduate
- 2010-2011, Spring, Seminars on Model Checking, Undergraduate
- 2010-2011, Autumn, Data Structure (in C), Undergraduate
- 2008-2009, Autumn, Requirement Engineering, Undergraduate (Leiden University)
- 2007-2008, Spring, Coordination and Composition, Graduate (Leiden University)
- I am currently interested in taking new PhD and master students every year. Please feel free to contact me if you are interested in any of the following topics: programming theory, software formal methods (especially model checking, theorem proving and constraint solving), cyber-physical systems, artificial intelligence, blockchain and smart contract, deep learning, quantum computing, and are exceptionally strong in mathematics (especially discrete mathematics, logic, algebra, differential equations and probability) or computer science. Students with strong programming skills are especially welcome.
- Domestic students could find the requirement and application process here.
- For international students, please send me your CV, research statement and a list of your publications (if you have) by email at least one year in advance of your expected start date.
- Details of the undergraduate student research topics and requirements can be found here.
- If you plan to go abroad for a PhD or Master degree, and hope me to write a reference letter for you, you must took at least two of my courses and got a score above 95 or A+ in all the courses, or took part in some undergraduate research project in my group and perform well in the project.
- PhD Candidates：
- LU Yuteng (2017)
- SUN Weidi (2018)
- XUE Xiaoyong (2019)
- BU Hao (2020)
- LUAN Xiaokun (2021)
- LI Xiangyu (2022)
- XU Ziyun (2022)
- Master Students：
- Bachelor Thesis:
- SHAO Kaicheng
- CHEN Zhirui
- Undergraduate Student Research:
- Seminar Information:
- The schedule of the group seminar can be found here.
- In 2019 autumn and 2020 spring semester, the junior graduate students and senior undergraduate students have a seminar on the book "Formal Methods: An Appetizer" by Flemming Nielson & Hanne Riis Nielson.
- In 2018 autumn and 2019 spring semester, the junior graduate students and senior undergraduate students have a seminar on the book "Introduction to Embedded Systems: A Cyber-Physical Systems Approach" by Edward Ashford Lee & Sanjit Arunkumar Seshia.
- In 2017 autumn and 2018 spring semester, the junior graduate students and senior undergraduate students have a seminar on the book "Introduction to Discrete Event Systems" by Christos G. Cassandras & Stephane Lafortune.
- In 2017 spring semester, the junior graduate students and senior undergraduate students have a seminar on the book "he Theory and Practice of Concurrency" by A. W. Roscoe.
- In 2016 autumn semester, the junior graduate students and senior undergraduate students have a seminar on the book "Principles of Cyber-Physical Systems " by R. Alur.
- In 2016 spring semester, the junior graduate students and senior undergraduate students have a seminar on the book "Communication and Concurrency " by R. Milner.
- In 2015 autumn semester, the junior graduate students and senior undergraduate students have a seminar on the book "Principles of Constraint Programming " by K. Apt.
- In 2014 autumn and 2015 spring semesters, the junior graduate students and senior undergraduate students have a seminar on the book "Principles of Model Checking " by C. Baier and J.-P. Katoen.
- PhD Students:
- Master Students:
- WANG Yiwu (2013-2016: master, After Graduation: China Unicom => Tencent), thesis: Extracting Coordination Models based on Active Learning.
- JI Yuanyi (2015-2019: master, After Graduation: Huawei), thesis: A Consensus Algorithm based on DPoS and its Security Proof
- XU Heyuan (2016-2019, After Graduation: AUKEY), thesis: Gas Usage Estimation Based on Regressive Analysis
- WANG Shun (2016-2019, After Graduation: China Unicom), thesis: The Application of Coalgebra Theory in Fuzzy Control Systems
- ZHANG Qi (2018-2021, After Graduation: China Telecom), thesis: Formal Modeling and Verification of the Nervos CKB Block Synchronization Protocol in UPPAAL
- FENG Yi-chun (2018-2021, After Graduation: Shopback), thesis: Modeling and Verification of CKB Blockchain Consensus Protocol Security
- YANG Xiaoyu (2019-2022, After Graduation: Peking University Third Hospital), thesis: Blockchain-Based Supply Chain Finance Design Patterns
- Bachelor Thesis:
- 2013: LI Yi (PhD candidate at PKU), Modeling and Analysis of Component Connectors in Coq (Published at FACS 2013)
- 2014: CHEN Xiaohong (PhD candidate at UIUC), A Hybrid Model of Connectors in Cyber-Physical Systems (Published at ICFEM 2014)
- 2014: HE Qi (Graduate student at MSU), Modeling and Implementing National Debt Database Based on UML
- 2015: LI Shaodong (Graduate student at NYU), A Framework for Off-Line Conformance Testing of Timed Connectors (Published at TASE 2015 and awarded as the conference best paper)
- 2015: JI Yuanyi (PhD candidate at PKU), Weakest Precondition and Loop Invariant of Probabilistic Programs
- 2016: XU Heyuan (Graduate student at PKU), Separation of Automata for Distributed Systems
- 2017: ZHANG Xiyue (PhD candidate at PKU), Reasoning about Connectors in Coq. (Published at FACS2016)
- 2017: HONG Weijiang (Graduate student at NUDT), Using Coq for Formal Modeling and Verification of Timed Connectors. (Published at FOCLASA 2017)
- 2017: LU Yuteng (Graduate student at PKU), Verification of the IEEE 802.11i Protocol Using UPPAAL (Published at SEKE 2018)
- 2018: SUN Weidi (PhD candidate at PKU), Generating PRISM Code from Mediator (Published at SEKE 2019)
- 2018: ZHANG Qi (Graduate student at PKU), Generating SystemC Code from Mediator (in Chinese, Published at Computer Engineering & Science)
- 2019: XUE Xiaoyong (PhD candidate at PKU), Probabilistic Extension of Mediator (in Chinese, Published at Computer Engineering & Science)
- 2020: BU Hao (PhD candidate at PKU), Modeling and Verification of CKB Block Synchronous Protocol in Coq (Published at ICFEM 2021)
- 2020: HUANG Xiankai, A Survey on Verification of Neural Networks
- 2021: LUAN Xiaokun, Modeling and Verification of CKB Consensus Protocol in Coq (Published at IEEE BSC 2021)
- 2022: XU Ziyun, Using Z3 for Formal Modeling and Verification of Timed Reo Connector
- Officially Funded Undergraduate Student Research:
- 2019-2020: LUAN Xiaokun: Using LSTM to Predict Tactics in Coq (Published at SEKE 2021)
- 2016-2017: FU Guirong: A Formal Design Model of Cloud Services (Published at SEKE 2017)
- 2013-2014: OU Yufei, LI Shaodong, Model Checking Business Processes for Web Service Compositions in mCRL2 (Published at IHMSC 2014).
- Visiting Students:
- 2016: YAO Yao (from Oxford University)
