教师主页移动版

陈明帅，研究员、博士生导师，CCF形式化方法专委与理论计算机科学专委委员，国家优秀青年基金（海外）获得者，入选浙江大学“新百人计划”、“启真学者”。2019年于中国科学院软件研究所获计算机软件与理论专业博士学位，导师为詹乃军研究员，同年获中国科学院院长特别奖（中科院软件所自1985年成立以来首获该奖项），此后赴德国RWTH Aachen从事为期3年的博士后研究工作，合作导师为Joost-Pieter Katoen教授。主要研究方向为程序语言、形式验证、数理逻辑、自动推理等，在Inf. Compt.、IEEE Trans. Automat. Contr.、OOPSLA、CAV、FM、ASPLOS、IJCAR、TACAS等多个顶级国际期刊或会议上发表学术论文20余篇，曾获ATVA 2018杰出论文奖、FMAC 2019最佳论文奖、Springer Nature计算机领域2020年中国学者1%高影响论文，曾任30余个国际期刊或会议的同行审稿人，并受邀在实时系统领域顶级国际会议RTSS 2020及ESWEEK 2022上做专题报告。主持国家优秀青年科学基金项目（海外）、浙江省自然科学基金重大项目、CCF-华为胡杨林基金形式化专项，作为项目骨干承担国家重点研发计划及浙江省尖兵领雁研发攻关计划，研究成果被成功应用于国家探月二期工程“嫦娥”三号软着陆、CTCS-3高速铁路控制等国家重大工程中的控制软件正确性保障中。陈明帅所领导的形式验证课题组旨在基于具有严格数学基础的形式化方法（模型检验、定理证明等），研发程序和离散-连续混成系统的形式验证与生成技术，以确保新型安全攸关信息物理融合系统的可靠性和有效性，并致力于推动验证与生成方法的自动化。具体研究方向包括（但不限于）：数理逻辑与形式化验证编程语言与程序理论信息物理融合系统概率与量子系统基于AI/ML的验证与生成课题组长期招聘/招收博士后、博士/硕士研究生和研究助理/实习生。更多信息请参见课题组网站Formal Verification Group。