讲授课程

  • 区块链原理、方法与应用，数学学院研究生课程（研本合上，隔年开设），2023-2024学年春季学期，课程主页在这里
  • 论文写作指导，数学学院研究生课程，2019-2024每学年春季学期，课程主页在这里
  • 程序设计技术与方法，数学学院本科生课程（本研合上），2017-2021每学年春季学期，2021-2024每学年秋季学期，课程主页在这里
  • 程序设计语言原理，数学学院研究生课程（研本合上，隔年开设），2022-2023学年春季学期，课程主页在这里
  • 软件理论讨论班，每学期开设，研究生、本科生均可参加
  • 数据结构与算法（B），全校本科生必修课程，2021-2022学年春季学期
  • 可信智能软件，数学科学学院本科生3+X讨论班，2021-2022学年秋季学期
  • 数据结构（Python语言），数学学院本科生课程，2015-2017及2018-2020每年秋季学期，课程主页在这里
  • AI理论讨论班，数学学院本科生3+X课程（面向大二、大三学生，无学分），2018-2019学年春季学期，课程主页在这里
  • 软件形式化方法（Model Checking），数学学院研究生课程（本科生可选），2015-2018每年春季学期（课程介绍）
  • 数据结构（C语言），数学学院本科生课程，2010-2014每年及2017-2018学年秋季学期，课程主页在这里
  • 集合论与图论，数学学院本科生课程，2012-2013学年春季学期，课程主页在这里
  • 软件理论与方法选讲（Algebraic and Coalgebraic Specifications），数学学院研究生课程，2010-2012每年春季学期
  • 低年级讨论班(信息)，数学学院本科生课程，2010-2011学年春季学期
  • Requirement Engineering，莱顿大学本科生课程，2008-2009学年秋季学期
  • Coordination and Composition ，莱顿大学研究生课程，2007-2008学年春季学期

回到顶部

研究生招生

  • 我一般每年招收博士生1-2人，含本科保送直博、申请审核制（已取得硕士学位或入学当年硕士毕业）两种形式，欢迎同学申请，建议申请前提前至少一年和我联系确认是否仍有招生名额。
  • 因招生政策调整，2021年之后学术型硕士生只招收港澳台及外籍学生（因学校选课要求，需有较好的中文水平），欢迎申请。
  • 可指导大数据专业硕士毕业论文，感兴趣的同学可入学后和我联系。
  • 如果你对程序理论、软件形式化方法、人工智能、深度学习、信息物理融合系统、区块链、信息安全、量子计算等领域感兴趣，希望从事相关的研究工作，并且具有很好的数学/计算机科学基础，欢迎申请加入我的课题组。
  • 对申请有助的信息（如有请在提交申请材料时重点强调）：
    • 在上述领域相关研究方向发表、录用或已完成投稿的高水平论文（中英文均可）或发明专利，需在其中有主要贡献，在理论框架、技术细节、算法思路、实验结果等方面能够经受考核；
    • 独立开发的较大规模系统或应用软件（代码量5000行以上，需提供源代码或开源链接，如有软件著作权证明可同时提供）；
    • 通过选修程序理论、形式化方法等方向相关课程、参加暑期学校或线上课程及阅读相关专著、论文的学习经历对我的某个研究方向有深入了解，需在个人陈述中进行详细说明；
    • 参加ACM ICPC（国际大学生程序设计竞赛）、CCPC（中国大学生程序设计竞赛）、阿里天池竞赛、华为软件精英挑战赛等各类程序设计竞赛的获奖经历。
  • 希望加入我课题组的同学请在正式申请前先和我联系确认是否仍有招生计划，建议在联系我之前先深入了解一下我的研究方向，更多内容可见这里关于研究生招生的介绍和要求。

回到顶部

本科生科研

  • 欢迎对程序理论、软件形式化方法、人工智能、深度学习、信息物理融合系统、区块链、信息安全、量子计算等领域感兴趣且学有余力，愿意从事相关研究工作的二、三年级本科生同学和我联系，参加我的讨论班及课题组研究活动。本科期间由我指导过本研且表现出色的同学在免试保研到本人课题组将予以优先考虑，或提供到其他高校或科研院所读研的推荐。
  • 部分本科生科研可选课题如下：
    • 深度学习系统的形式化模型构建与合成
    • 基于模型的深度学习系统测试理论与方法
    • 深度学习系统形式化验证技术
    • 区块链共识协议与智能合约功能正确性、安全性的形式化建模与验证
    • 区块链智能合约规约语言设计
    • 信息物理系统复杂交互行为的统计模型检查方法
    • 基于深度学习的模型检查反例生成方法
    • 基于深度学习的定理证明自动化技术
    • 概率实时系统 / 信息物理系统 / 量子系统的余代数模型和余归纳推理方法
    • Mediator建模语言的混成扩展及相关工具实现
  • 要求：
    • 对课题相关领域感兴趣且具有较高的科研热情，做事认真负责，具有创新精神和独立工作能力且愿意与他人合作，英语读写能力强，有较好的编程能力（数学建模能力较强者更佳）；
    • 对自己的时间能够有很好的规划安排，需在学有余力的情况下参与项目工作，学期中至少需保证每周8-10小时用于项目工作的时间（每周参加课题组讨论班，阅读文献，编程实现及论文写作），假期至少保证1/2的时间用于项目工作。
  • 注意：
    • 课程成绩并非我考虑的主要因素，我更看重的是学生的兴趣和态度，如果你能够很好地规划时间安排，完全可以把科研工作和课程学习两者都做好，但因为参加本研需投入较多的时间和精力，如果你的兴趣不在我的研究方向上请考虑其他老师；
    • 部分课题的研究需要一定的知识储备，可能你在从事课题研究之前，需要先选修一些相关课程并阅读部分我推荐的文献；
    • 学校官方的本研项目对申请人绩点有一定的要求（比如有些项目要求申请人绩点不低于3.3），如果你未达到这一要求但对本人研究感兴趣且愿意投入时间精力从事相关研究，或者不愿花费太多时间在各种文字材料上（学校的本研项目中期和结题都要提供报告），也可以直接联系我，申请加入我的课题组从事本研工作，虽然无法受上述项目资助，但从事研究的相关费用（文献资料费、论文发表版面费、会议注册费、差旅费等）可受本人科研项目经费支持，且灵活度相对更高。
  • 报名方式：
    • 通过email报名，提供个人基本信息（姓名、学号、电话、email等），是否对我的方向已有所了解，读过哪些论文或专业书籍（除教材之外），如已选定课题请在邮件中说明，并安排时间和我面谈一次。

回到顶部

本科生毕业论文

  • 我2024-2025年每年可指导最多3位同学的本科生毕业论文，希望我指导本科生毕业论文的同学，需于大四上学期开学日之前和我联系。晚于此日期后请联系其他老师。

回到顶部

推荐信

  • 原则上我只会为了解的同学推荐，自2023年起，因出国或保研至其它单位希望我写推荐信的同学，需至少满足下列两者之一：
    • 跟我做本科生科研并有被我承认的较好成果，
    • 选修过至少两门我的课程，且每门课期末总评成绩均在95分以上（若只满足这一条，我将仅在推荐信中提供课程成绩说明而不会提供除此之外的任何推荐意见），
  • 不符合以上条件的同学请联系其他老师。

回到顶部

当前指导学生

  • 博士：
    • 薛骁勇（北京大学数学科学学院，信息科学系，2019年直博入学）
    • 卜昊（北京大学数学科学学院，信息与计算科学系，2020年直博入学）
    • 栾晓坤（北京大学数学科学学院，信息与计算科学系，2021年直博入学）
    • 李翔宇（Georgia Institute of Technology，Master in Electrical & Computer Engineering，2022年申请审核制博士入学）
    • 徐紫云（北京大学数学科学学院，数据科学与大数据技术专业，2022年直博入学）
    • 邵凯诚（北京大学数学科学学院，信息与计算科学系，2023年直博入学）
  • 硕士：
    • 周东旭（北京大学数学科学学院，2022级应用统计硕士）
    • 周宇洋（北京大学数学科学学院，2023级大数据硕士）
  • 本科生毕业论文：
    • 张益豪（北京大学数学科学学院，2020级数据科学与大数据技术专业本科生，保送直博，2023-2024年访问新加坡管理大学）
  • 本科生科研：
    • 魏泽明（北京大学数学科学学院，2021级）
    • 卢天泽（北京大学数学科学学院，2021级）
    • 岳关璋（北京大学数学科学学院，2022级）
  • 讨论班：
    • 本学期研究生讨论班日程安排见这里。
    • 2023年秋季低年级研究生及高年级本科生讨论班内容：“Introduction to Static Analysis”, Xavier Rival & Kwangkeun Yi著。  
    • 2019年秋季及2020年春季低年级研究生及高年级本科生讨论班内容：“Formal Methods: An Appetizer”, Flemming Nielson & Hanne Riis Nielson著。
    • 2018年秋季及2019年春季低年级研究生及高年级本科生讨论班内容：“Introduction to Embedded Systems: A Cyber-Physical Systems Approach”, Edward Ashford Lee & Sanjit Arunkumar Seshia著。
    • 2017年秋季及2018年春季低年级研究生及高年级本科生讨论班内容："Introduction to Discrete Event Systems"，Christos G. Cassandras & Stephane Lafortune著。
    • 2017年春季低年级研究生及高年级本科生讨论班内容：“The Theory and Practice of Concurrency”， A. W. Roscoe著。
    • 2016年秋季低年级研究生及高年级本科生讨论班内容：“Principles of Cyber-Physical Systems”. Rajeev Alur著。
    • 2016年春季低年级研究生及高年级本科生讨论班内容：“Communication and Concurrency”, R. Milner著。
    • 2015年秋季低年级研究生及高年级本科生讨论班内容：“Principles of Constraint Programming”，K. Apt著。
    • 2014年秋季及2015年春季讨论班内容：“Principles of Model Checking”，C. Baier & J. P. Katoen著。
    • 2014年春季讨论班内容：“Concurrency Theory: Calculi and Automata for Modeling Untimed and Timed Concurrent Systems”，H. Bowman & R. Gomez著。
    • 2013年秋季讨论班内容：“Communicating Sequential Processes” ， C. A. R. Hoare著。

回到顶部

往年指导学生

  • 博士生（学位论文全文仅限北京大学校内访问）：
    • 李屹，2013年本科毕业于北京大学数学科学学院信息科学系，2013-2019年硕博连读，获2013-2014、2015-2016、2016-2017年度国家奖学金、2016-2017、2017-2018、2018-2019年度校长奖学金、2017-2018年度五四奖学金、2014-2015年度廖凯原奖学金，曾于2014年访问新加坡科技设计大学，2017年访问德国萨尔大学，2019年7月博士毕业，学位论文《Coordination and Composition: From Reo to Mediator》（abstract，fulltext），2019年入职华为（天才少年计划）。
    • M. Saqib Nawaz Khan，2014年硕士毕业于University of Sargodha，2015-2019年普博，获2018-2019年度北京大学留学生学习优秀奖，2019年7月博士毕业，学位论文《Using UTP and PVS for Formal Verification of Composition and Coordination Models》（abstract，fulltext），2019-2022年任职哈尔滨工业大学（深圳）博士后，2022年起任职深圳大学计算机与软件学院副研究员。
    • 刘艾，2015年本科毕业于中国科学技术大学少年班学院，2015-2020年直博，获2015-2016年院长奖学金，2018-2019年度方正奖学金，曾于2018年访问葡萄牙Minho大学，2020年7月博士毕业，学位论文《Coalgebraic Semantics for Complex Component-based Systems》（abstract，fulltext），2020-2023年任职日本广岛国立大学助理教授，2024年起任职南京航空航天大学特聘副研究员（国家级青年人才）。
    • 张喜悦，2017年本科毕业于北京大学数学科学学院信息科学系，2017-2022年直博，获2019-2020、2020-2021年度国家奖学金、2017-2018、2018-2019、2019-2020、2020-2021年度校长奖学金、2017-2018年度五四奖学金、2018-2019年度廖凯原奖学金，曾于2017年访问新加坡科技设计大学，2019-2020年访问新加坡南洋理工大学，2022年7月博士毕业，学位论文《Towards Trustworthiness Assurance of Deep Learning Systems with Certification Techniques》（abstract，fulltext），获北京大学优秀博士学位论文奖，2022年北京大学优秀毕业生，2022年起任职英国牛津大学副研究员。
    • 卢煜腾，2017年本科毕业于北京大学数学科学学院，2017-2023年硕博连读，获2017-2018年度国家奖学金、2018-2019、2019-2020年度北京大学三好学生，2019-2020年度研究生专项学业奖学金、2021-2022年度秦宛顺靳云汇奖学金，2021-2022年度学术创新奖，2022-2023年度五四奖学金，2022-2023年度北京大学优秀学生干部，2023年7月博士毕业，毕业论文《Testing-based Machine Learning System Safety Strengthening》（abstract，fulltext），2023年北京大学优秀毕业生，2023年起入职中国舰船研究院。
    • 孙纬地，2018年本科毕业于北京大学元培学院，2018-2023年直博，获2018-2019、2019-2020、2020-2021年度学院奖学金，2019-2020年度优秀科研奖，2021-2022年度校长奖学金，2022-2023年度斯伦贝谢奖学金，2022-2023年度北京大学三好学生，2023年7月博士毕业，毕业论文《Coverage Testing and Global Verification of Deep Learning Systems》（abstract，fulltext），2023年入职华为。
  • 硕士生：
    • 王译梧，2013年本科毕业于山西大学数学学院，2013-2016年硕士，获2014-2015年度光华奖学金，2016年7月硕士毕业，学位论文《基于主动学习的协调模型生成》，毕业后先后任职于联通、腾讯，现就职于润联软件系统(深圳)有限公司。
    • 冀元祎，2015年本科毕业于北京大学数学科学学院，2015-2019年硕士，获2015-2016年度校长奖学金，2019年硕士毕业，学位论文《一个基于DPoS共识算法的设计与安全性证明》，毕业后任职于华为。
    • 徐鹤元，2016年本科毕业于北京大学数学科学学院，2016-2019年硕士，2019年硕士毕业，学位论文《基于回归分析的燃气用量估计》，毕业后任职于傲基科技，现就职于博时基金。
    • 王顺，2016年本科毕业于首都师范大学数学学院，2016-2019年硕士，曾于2018年访问葡萄牙Minho大学，2019年硕士毕业，学位论文《余代数理论在模糊控制系统中的应用》，毕业后任职于联通。
    • 张琦，2018年本科毕业于西安电子科技大学计算机学院，2018-2021年硕士，获2017-2018、2018-2019年度研究生专项奖学金、2019-2020年度帝人奖学金，2021年硕士毕业，学位论文《基于UPPAAL的Nervos CKB区块同步协议的形式化建模及验证》，2021年北京大学优秀毕业生，毕业后任职于中国电信研究院。
    • 冯逸群，2018年本科毕业于台湾大学工学院，2018-2021年硕士，获2020年台湾硕士奖学金一等奖，2020-2021年度研究生专项奖学金，2021年硕士毕业，学位论文《CKB区块链共识协议的安全性建模与验证》，毕业后任职于Shopback。
    • 杨晓宇，2019年本科毕业于河北师范大学软件学院，2019-2022年硕士，获2021-2022年度北大三等奖学金，2022年硕士毕业，学位论文《基于区块链的供应链金融设计模式》，2022年北京市优秀毕业生，毕业后任职于北医三院。
    • 李忆，2020年本科毕业于武汉大学数学与统计学院，2020-2023年硕士，2023年硕士毕业，学位论文《Stellar共识协议的形式化建模与验证》，2023年北京大学优秀毕业生，毕业后任职于重庆市发改委。
    • 廖佳威，2021-2023年应用统计专业硕士，2023年毕业，学位论文《无许可区块链的动态分片扩容算法研究——基于PotER-PPOSB和DQNSB的对比研究》。
  • 本科生（毕业论文 / 本科生科研）：
    • 姓名 毕业时间暨院系 / 专业 毕业去向 本科生科研 毕业论文
    李屹
    2013.7信息科学系
    本系保研
    		  
    2014.7信息科学系
    伊利诺伊大学香槟分校
    		  
    何麒
    2014.7金融数学系
    密歇根州立大学
    		  
    基于UML的国债数据库系统建模与实现
    李少东
    2015.7信息科学系
    纽约大学
    		 Model Checking Business Processes for Web Service Compositions in mCRL2 （IHMSC2014，校长基金*）
    2015.7信息科学系
    哥伦比亚大学
    冀元祎
    2015.7概率统计系
    本系保研
    		  
    概率程序最弱前条件与循环不变量
    2016.7信息科学系
    本系保研
    		 
    分布式系统的自动机拆分
    2017.7信息科学系
    本系直博
    		 
    卢煜腾
    2017.7信息科学系
    本系保研
    		 
    洪伟疆
    2017.7信息科学系
    		 保研国防科大  
    伏贵荣
    2018.7元培学院
    ETH Zurich
    		 A Formal Design Model of Cloud Services (SEKE 2017，校长基金*)
    孙纬地
    2018.7元培学院
    本系直博
    		 
    张琦
    2018.7计算机学院（西安电子科技大学）
    本系保研
    		 
    薛骁勇
    2019.7信息科学系
    本系直博
    		  Mediator建模语言的概率扩展（《计算机工程与科学》）
    卜昊
    2020.7信息与计算科学系
    本系直博
    		  Modeling and Verification of CKB Block Synchronous Protocol in Coq (ICFEM 2020)
    黄贤凯
    2020.7信息与计算科学系
    就业
    		   神经网络验证综述
    栾晓坤
    2021.7信息与计算科学系
    本系直博
    		Using LSTM to Predict Tactics in Coq (SEKE 2021，北京市创新计划*) Modeling and Verification of CKB Consensus Protocol in Coq (BSC@QRS 2021)
    徐紫云
    2022.7数据科学与大数据技术
    本系直博
    		Using Z3 for Formal Modeling and Verification of Timed Reo Connector（SERP 2023）
    邵凯诚
    2023.7信息与计算科学系
    本系直博
    		Extracting Automata from Extensive-Form Games Policies
    2023.7数据科学与大数据技术
    阿姆斯特丹大学
    		 Modeling and Verification of Producer-Consumer Communication in Kafka via Mediator
    2024.7数据科学与大数据技术
    本系直博
    		 Using Z3 for Formal Modeling and Verification of FNN Global Robustness（SEKE 2023） Extracting Automata from Attention-based Deep Learning Framework
    2025.7数据科学与大数据技术（expected）
     
    		 Extracting Weighted Finite Automata from Recurrent Neural Networks for Natural Languages（ICFEM 2022）  

    上表所列本科生科研内容标*者为受学校资助正式立项的本科生科研项目，其他为课题组经费支持项目，多位同学的毕业论文为其受课题组经费支持所从事的本科生科研工作内容。

回到顶部