所在实验室主页：系统可信性自动验证国家地方联合工程实验室-- 形式化系统研发中心

 

至未来成员：仅限以研究或开发类工作为职业目标者，热爱学习、不惧挑战！提供系列行业学习与交流的相关条件。

对确定进入团队的同学，提前安排相关背景知识、开发工具的学习。

部分研究课题与吴贯锋博士(英国女王大学博士后)联合指导，吴老师目前从事AI多模态、SAT验证、自动推理相关研究。

目前每年招收研究生约4名，如果您评估后可以较好地匹配以下3条中的2条，欢迎发送正式邮件联系(需提供：简历1份，成绩单及相关证书证明材料)！

(1) 学习过嵌入式系统开发，如51单片机、STM32开发板等，调试过传感器件，对智能交通系统场景有较浓兴趣；(2) 喜爱研发工作，并以研发为职业目标(如有Github主页项目展示，熟悉Linux系统等)；(3) 邮件与文档版式细致、规范，有较高的学研与就业目标，或有进一步深造的需求。

---- 2024.01.04

 

组内研究生(独立或联合指导)—含部分成员主页链接：

2024级 杨帆(计算机科学与技术)。

2024级 孙宝琦(软件工程-学)。

2024级 张莹(推免，软件工程)。

2024级 吴林蔚(推免，软件工程)。

2023级 Haider Abbas(计算机科学与技术)。

2023级 白仕博(推免，计算机技术)。

2023级 杨宇轩(软件工程)。

2023级 陈骊(软件工程)。

2023级 刘铸纬(计算机科学与技术)。

2023级 丁晨旭(计算机技术)。

2022级 罗照海 (计算机技术)。

2022级 蒋滨 (推免，计算机科学与技术)。

2021级 陈顺(计算机技术)，签约至四川农商银行 成都。

2021级 刘昱含(推免，交通信息工程及控制)，签约至成都中国电科30所。

2021级 赵大地(推免，交通信息工程及控制)，签约至郑州中船集团713研究所。

2020级 李尔涛(交通运输工程)。在卡斯柯公司联合培养，并从事形式化建模验证与切片算法研究课题。入职成都中国电科30所。

2020级 冯心妍(交通运输工程)，大四下学期开始形式化验证学习。SAT求解器算法研究课题。交通运输专业攻读博士学位。

2020级 王梓(推免，交通信息工程及控制)，大四上学期开始在团队学习，并通过毕业设计掌握了1门形式化建模语言，并获优秀毕业设计。智能合约转换算法及验证研究课题。入职北京全路通信信号研究设计院。

2020级 张丁荣(推免，交通信息工程及控制)，大四上学期开始在团队学习，并通过毕业设计掌握了1门形式化建模语言。事故库的知识图谱与割集求解算法研究课题。入职北京和利时集团中央研究院。

2019级 唐伟健 (交通信息工程及控制)，除实验室学习外，多次参加了学科活动与企业实践，合作发表论文表3篇，其中1作1篇。已入职至 北京和利时系统工程有限公司。

2018级 程鹏 (交通运输工程)，大四下学期开始形式化验证学习，目前较好地掌握了验证中的证明过程，论文已发表5篇，其中1作3篇。已入职北京铁道科学研究院。

2018级 刘宁 (计算机技术)，大四下学期开始形式化验证学习，目前具备了基于验证开发的较好能力，论文已发表4篇，其中1作2篇；参加为期近10天的第二届研究生海外研学活动，赴新加坡研学。已入职成都楠菲微电子有限公司。

2017级 王峥 (交通运输工程)，硕士期间发表论文3篇，获国家奖学金、交控奖学金，在里斯本、西南大学各进行1次英文学术报告，并入选首届“双一流”学生全球胜任力提升项目，赴日本研学实践。已入职 北京全路通信信号研究设计院。目前在北京航天三院从事磁浮飞车运控系统的研发。

2016级 王霞 (推免，交通运输规划与管理)，参加研究生支教团1年；硕士阶段参加了多次形式化验证领域的学科活动，并进行1次英文学术汇报，论文发表(录用)4篇。硕博连读，转为2020级计算机科学方向博士生，2024.4 清华大学博士后。

2015级 张黎青 (交通运输工程)，已获澳门大学 智能交通方向 全额博士生奖学金。

2014级 张传东 (推免，控制工程)，大四下学期开始形式化验证学习，获校级优秀毕业设计；研究生阶段是PLC验证项目的核心成员。签约至北京和利时系统工程有限公司工作，已成长为列控系统研发骨干。目前在交大盛阳继续从事信号与列控系统的研发攻关。

 

研究生培养方式：康乐、严谨、合作、高远

Ø  与学生共同制定成长规划，脚踏实地做好核心能力建设工作。

Ø  努力营造奋进、愉悦的学习与沟通氛围，并通过各类方式帮助学生减小生活负担。

Ø  按个人规划，帮助学生联系行业单位实习，并大力支持学生参加国内外学术与技术研讨活动，锻炼学术交流能力，扩展科研视野。

 

科创指导

指导个性化实验项目、重点实验室开放项目、SRTP项目。

项目内容主要为：嵌入式系统开发、智能交通系统开发验证应用等方向。

团队成员常年指导本科生约10名左右，并提供相应开发条件，欢迎申报时进行联系。

已指导学生团队获得教育部A类学科竞赛 决赛奖项20多项。

 

部分团队活动(以2018.7-2019.12期间为例)：

·       2019.12，团队成员刘宁参加了第二届研究生海外研学活动，赴新加坡南洋理工大学等单位研学10天，主题：交通运输规划。

·       2019.11.30-12.2，团队成员唐伟健赴上海华东师范大学，参加中国计算机协会第四届全国形式化方法与应用年会（FMAC2019）。

·       2019.11.14-20，英国南安普顿大学形式化方法团队Dr. Colin高级研究员受邀访问实验室，讲座两场，并与大家共同探讨工业验证领域难题的解决方法。

·       2019.11.8-14，刘宁赴广州参加ICECCS2019形式化国际会议。

·       2019.11.3-9，王霞、程鹏赴深圳参加ICFEM2019形式化国际会议。

·       2019.11.5-7，王恪铭、王峥赴上海参加Prover公司组织的列控验证产品交流会，与该公司技术人员及行业研究人员进行了广泛的交流、讨论。

·       2019.10，王峥获国家奖学金、交控奖学金，并入围唐立新奖学金评选。

·       2019.8.22-23，王恪铭受邀作为评审专家，赴北京通号设计院参加科技部专项课题区域轨道交通研究子课题的评审。

·       2019.8.3-8.9，程鹏赴上海科技大学参加 形式化方法 国际暑假研讨班。

·     2019.7.31-8.1，团队研究成果入选First International Workshop on Knowledge and Model-driven engineering in TASE 2019 (13th International Symposium on Theoretical Aspects of Software Engineering)，研究生王霞于7月底赴桂林做学术报告（29 July – 1 August 2019, Guilin, China），王恪铭为该会议的程序委员。

·       2019.7.8-7.12，团队研究生王霞入选上海可信人工国际暑假学校，参加了为期一周的学习，该暑假学校师资由英国、美国、新加坡等大学的专家学者组成。

·       2019.7.2-8.25，团队王恪铭博士与王峥、程鹏、刘宁3位研究生赴通号院粤港澳分公司，开启为期两个月的实习、合作对接工作。

·       2019.6-8月，团队成员唐伟健赴北京和利时系统工程有限公司，进行列控产品研发岗位的实习。

·       2019.4.20-4.27,团队成员共赴重庆西南大学，第五届可信软件系统工程（国际）春季学校（SETSS 2019），研究生王峥在Workshop中做铁路系统验证的英文报告。

·       2019.3-6月，团队研究生王霞获批唐山研究生院科研培育项目，赴唐山开展科研交流。

·       2019.1.22-26，团队王恪铭博士随铁路信息工程系代表团访问日本，并在东日本铁路公司、日本信号公司、京三信号公司进行技术交流。

·       2018.11.11-21，团队研究生王峥，入选研究生院“双一流”学生全球胜任力提升项目，赴日本研学实践。

·       2018.11.3-4，团队成员共赴重庆西南大学，参加中国计算机协会第三届全国形式化方法与应用年会（FMAC2018）。

·       2018.10.15，团队王恪铭博士结束在英国University of Southampton，ECS两年的博士后研究工作，返回实验室。

·       2018.7.2-7.5，团队研究生王峥赴欧洲Lisbon, Portugal，参加16th International Conference on Railway Engineering Design & Operation, 并做联锁系统数据验证的报告。