符鸿飞：科技推手——形式化方法

21世纪，我们生活在全新的科技时代，科技更新换代的速度，让世界的每一秒都处在不断变化当中。而变化的推手，正是那些兢兢业业的科研人员，他们用智慧推动着世界的发展。

符鸿飞就是他们中的一员，他长期从事形式化方法研究，着重理论联系实际，推动成果转化，心无旁骛地孜孜以求，在该领域里，取得了丰硕的科研成果。

创新研究 让形式化方法更上一层楼

在符鸿飞看来，形式化方法是利用数学和逻辑的方法证明计算机系统正确性的研究领域。作为理论计算机科学的一个重要分支，它为关键系统组件正确性的自动化推理和证明提供了坚实的基础，因此能够为系统是否满足一些关键的正确性性质作出最强的保证。

模型检测和程序验证是符鸿飞的两个重要研究方向，通过兢兢业业的付出，取得了突破性进展。对形式化方法有所研究的人都知道，模型检测是研究如何验证系统模型正确性的研究领域。在模型检测方面，符鸿飞将精力放在研究概率模型检测的算法、可判定性和计算复杂性领域，并在这些领域取得了基础性理论成果。

在模型检测算法方面，符鸿飞以独立作者身份给出了关于连续时间马尔可夫过程时序逻辑的两个基础模型检测算法，并发表在国际著名形式化方法学术会议FOSSACS、HSCC上。而在可判定性和计算复杂性理论方面，符鸿飞则将研究重点放在了离散时间马尔可夫过程上关于互模拟等价关系的可判定性和计算复杂性，并以独立作者或主要贡献者身份在国际著名理论计算机科学学术会议ICALP、FSTTCS等上发表多篇重要论文。

相对于模型检测，程序验证是研究如何验证程序正确性的方向。在程序验证方面，符鸿飞在程序终止性以及运行时间验证方面取得诸多基础性理论结果，并发表在国际顶级形式化方法、程序语言理论以及人工智能学术会议POPL、CAV、IJCAI上。首先，他作为主要贡献者与合作者提出了分级上鞅在同时带有恶意非确定性与友善非确定性概率程序上的定义，并给出了线性分级上鞅的合成算法以及相关的计算复杂性，进而为带有非确定性的概率程序终止性与期望运行时间验证提供了一个坚实的理论基础；同时，符鸿飞在该成果中证明了分级上鞅可以导出有限步内不终止概率的指数衰减性。其次，他通过实代数几何中的一些数学定理以及半正定规划给出了概率程序上合成多项式分级上鞅的一个高效算法，并将分级上鞅的方法推广至概率程序的资源消耗验证。最后，符鸿飞将分级函数推广至不带概率的递归程序，进而通过线性规划以及实代数几何上的一些定理给出了一个输出递归程序精确运行时间的验证算法；该算法可以有效地输出很多经典递归算法（如归并排序、最近点对算法等）的精确非多项式运行时间；同时，符鸿飞基于一元递归关系针对随机递归算法给出了一个验证精确期望运行时间的高效算法；该算法可以在线性时间内输出一个由随机递归算法导出的递归关系的精确期望运行时间。

功夫不负有心人，任何的付出，都会在成绩上得到体现，目前，符鸿飞在理论计算机科学以及形式化方法国际著名会议以及期刊上发表论文15篇。获得过HSCC 2013最佳学生论文奖以及科学中国人2017年度人物。

作为一名科研工作者，符鸿飞勇于承担更多的责任，在研究中，他承担了一项关于大规模并发实时系统模型检验的国家重点项目。该项目的重点在于研究新的理论方法以有效验证兼具随机性、并发性以及实时性特征的大规模系统。随机性、并发性以及实时性都是难以通过直觉或是大规模测试保证正确性的复杂系统性质。通过该项目的研究，能够在为保证大规模概率并发实时系统关键性质方面给出一个有效的理论框架。

面向未来  换位思考做好教学工作

“师者，所以传道受业解惑也。人非生而知之者，孰能无惑？惑而不从师，其为惑也，终不解矣。”对于这句话，符鸿飞有着更深刻的理解和体会。

作为一名孕育桃李的师者，他将学生放在首位。在教学方面，他突破传统，从学生的角度考虑讲课风格，比如在设计教学内容的时候考虑什么样的内容是有助于学生的，在进行教学的时候站在学生的角度看待问题、设想学生会如何去学习新的知识。

在符鸿飞看来，每个学生都是独立的存在，在学习一门课程前都有属于自己的知识结构，如果教师严格按照自己对课程内容的把握上课，有可能会导致学生无法将新的知识同原有的知识结构建立起联系，因此换位思考十分必要，从学生的角度出发设置课程，推进教学方法改革，有助于学生能够循序渐进地掌握课程内容。

由于学生自身情况各不相同，在掌握课程内容方面多有差异，因此教师要对每个学生都耐心、尽量解决每个学生的问题。

课堂气氛是符鸿飞教学的关注点之一，调动学生的积极性，教师不在唱独角戏，学生由被动接受变为主动探讨，活跃课堂气氛，有助于提升学生的注意力，提高其参与课程的积极情绪，从而提升教学效果。

在课程内容的设置方面，他联系专业背景，力求学生在修习过课程后能够更好地适应专业发展趋势。讲课时须要注意保持讲课逻辑的一致性和内在关联性，使得学生能够融会贯通，并随时观察学生掌握课程内容的情况并进行有必要的干预。

作为科研工作者，符鸿飞奋斗在科研第一线，用锲而不舍的创新精神，攀越一座又一座科研高峰；作为师者，他突破传统教学方式，换位思考，对教学进行创新改革。

科研和教学之路还在继续，他将用智慧继续书写属于自己的奋斗人生……