扎实打根基 创新展宏图——记上海交通大学电子信息与电气工程学院特别副研究员符鸿飞

◎ 文/曹 莉

他对科研的态度是严谨治学、打牢根基。他创新的 “形式化验证”是一种从理论上进行测试的全新方法，被形象地称作为 “穷尽式数学技术”，其原理是利用数学和逻辑的方法来证明计算机系统的正确性。

他长期致力于理论计算机科学中的形式化验证领域研究，在获得一系列原创性理论成果的同时，紧密结合工业界生产实际，致力于把理论成果成功地转化为工业实践，并取得了丰硕的成果。

他的学术成就丰富，在理论计算机科学、形式化方法国际著名学术会议及期刊上以主要贡献者身份发表论文14篇，为ICALP、VMCAI、FOSSACS、Information and Computation、Information Processing Letter等审稿30余篇，参与国家自然科学基金重点项目1项，获得国家自然科学青年基金资助1项，曾获HSCC 2013年度最佳学生论文奖以及科学中国人2017年度人物。

他就是上海交通大学电子信息与电气工程学院特别副研究员符鸿飞。

热爱专业领域,迈向纵深地带

作为学者，符鸿飞是个爱学习爱钻研的人。任何一门学科，任何一个专业要想深入学习了解，真正掌握其中的奥秘，就必须有无比热爱的胸怀和敢于向纵深地带不断探索前进的精神。符鸿飞的身上具有这种科研的精神特质，这种特质来自于他对专业领域不断学习、研究和攻关。

当他回忆起自己的成长之路时，心情一如阳光那般灿烂。2003年，他考入上海交通大学计算机科学与技术专业。他说：“当时之所以会选择计算机专业是因为想探索与数学有一定联系的计算机问题。”他清楚地记得自己在读本科期间对如何保证程序编写的正确性产生过困惑，因此在写完程序后往往会反复读几遍程序，确保程序不会出错。而这种写程序的方法与通常测试检验程序的方法相比速度比较慢，但通过这种写程序的方法又有缺陷较少的优点，使后期调试过程变得相应较短。他兴奋于自己的研究发现，加速了他向形式化验证这个纵深领域迈进的步伐。

符鸿飞真正对利用数学方法证明系统正确性的形式化验证领域产生浓厚兴趣的是在他硕士研究生阶段。攻读研究生期间，他选择了上海交通大学傅育熙教授作为自己的导师。傅教授的研究方向是理论计算机科学中的进程理论。正是在傅教授的指导下，符鸿飞对一些无穷状态进程模型的可判定性和计算复杂性进行了全面系统的研究，并在互模拟判定以及模型检测算法方面作出了理论上的贡献。

学习最大的乐趣就是不断有新发现新方向，从而不断挺进纵深研究地带。为把形式化验证学透搞通，形成形式化验证的一套方法体系，他通过国家公派留学找到了该领域著名学者Joost-Pieter Katoen教授，赴德国亚琛工业大学攻读与形式化验证相关的博士。期间，他重点研究了概率系统形式化验证，独自给出了诸多相关理论问题的基础算法和计算复杂性，并逐渐由纯理论转向理论与应用相结合。在花费4年时间攻读完博士并拿到学位后，符鸿飞又踏上了博士后研究的征程，与奥地利科学技术研究院（IST Austria） 的Krishnendu Chatterjee教授合作研究概率程序的形式化验证，并发表了多篇关于基础理论的结果。

随着严谨求学的不断深入，他逐渐形成了一个观点，那就是程序验证（即针对程序的形式化验证）领域是理论和应用相结合的一个范例，在理论上可以开拓新的形式化验证领域，在应用上也可以和无运行时错误保证、无安全漏洞等重要的实际应用相结合。而程序验证方向也同他本科时遇到的如何保证写对程序这个问题高度一致。这令他甚感欣慰。

2017年，他带着回报祖国、感恩母校的情怀从国外归来，一如自己所愿，成为上海交通大学电子信息与电气工程学院集体的一分子，并任特别副研究员，这让他倍感荣幸与快乐。在此，他开始新的科研跋涉之旅，但他不问艰辛只管耕耘。

创新关键成果,推进科学发展

计算机系统的正确性在安全或任务关键系统中是一个核心课题。由于潜在的漏洞可能导致重大的人生或财产损失，如何保证关键系统不出现重大漏洞是一个重要的问题。

近年来，随着计算机系统越来越复杂，通过传统测试方法越来越难以覆盖足够多的系统执行路径。因此，致力于理论计算机科学中的形式化验证领域研究的符鸿飞利用数学和逻辑的方法来证明计算机系统研究领域的正确性，在理论背景和实际应用成果上可知，形式化验证为全覆盖的、自动化的系统正确性证明提供了一个行之有效的方法。作为理论计算机科学的一个重要分支，形式化验证为关键系统组件正确性的自动化推理和证明提供了坚实的基础，因此能够为系统是否满足一些关键的正确性性质作出了可靠保证。

形式化验证中的模型检测和程序验证是他研究的两个重要方向，他付出了很多心血，做出了重大贡献。说起模型检测问题，其实就是研究如何验证系统模型正确性的研究领域。他着力研究概率模型检测的算法、可判定性和计算复杂性，并获得了一些基础性理论成果。在模型检测算法上，他以独立作者身份给出了关于连续时间马尔可夫过程时序逻辑的两个基础模型检测算法，并发表在国际著名形式化验证学术会议FOSSACS、HSCC上。其中发表在HSCC上的论文获得了最佳学生论文奖。在可判定性和计算复杂性理论方面，他着力研究离散时间马尔可夫过程上关于互模拟等价关系的可判定性和计算复杂性，并以独立作者或主要贡献者身份在国际著名理论计算机科学学术会议ICALP、FSTTCS上发表多篇重要论文。

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

创新是科研的灵魂。符鸿飞觉得在形式化验证这个研究领域的创新有三种成果：一是通过复杂的数学方法解决一个已经被提出的公认难题；二是创新可以通过提出新的理论概念、并通过充实的依据说明提出的概念具有理论或实际上的意义；三是创新还可以通过将理论成果应用到大规模工业系统中，以验证实际系统中的一些关键性质。

作为导师，他在上海交通大学带领博士生进行形式化方法深入研究，并教授《离散数学》、《程序语言理论》等与形式化验证相关的课程。同时，他与博士导师Joost-Pieter Katoen教授、博士后合作导师Krishnendu Chatterjee教授以及一些国内著名学者保持合作关系，致力于推进形式化验证的更大发展。

对从事教学与科研的专家来说，科学研究最重要的就是传承，科研成果的取得需要一代代科研人在承上启下中再创新高。符鸿飞真切地希望通过自己悉心传教，尽早培养出一批具有扎实专业知识基础、能够独立自主开展科研工作的学生，进一步探索如何将所创理论更多地应用于丰富的实践中，推动学科专业迈向科学的顶峰。