——记上海交通大学计算机科学与工程系符鸿飞

　　当今之世，电子计算机技术和以其为基础的互联网科技正深刻地改变着人类的生产和生活。与此同时，计算机和互联网的效率和安全问题也就成为摆在人们面前的一项重要课题。在计算机硬件(特别是集成电路)和软件系统的设计过程中，形式化方法是根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。上海交通大学电子信息与电气工程学院特别副研究员符鸿飞长期致力于形式化方法的研究事业，并着重于理论联系实际，尽量将理论成果实现现实生产生活的运用，取得了丰硕的成果。

　　在兴趣指引下孜孜以求

　　爱因斯坦有句名言：兴趣是最好的老师。但凡要在一项事业中取得成绩，离不开日复一日的辛勤耕耘。同时，如孔夫子所言，好之者不如乐之者。从事研究工作，最好是在兴趣的促使下，心无旁骛地孜孜以求。符鸿飞正是这么做的。

　　符鸿飞于2003年考入上海交通大学计算机科学与技术专业。之所以当时会选择计算机专业是因为想探索与数学有一定联系的计算机问题。在本科求学期间，在编写程序的过程中，符鸿飞对如何保证程序编写的正确性产生了困惑，因此在写完程序后往往会反复读几遍程序，确保程序真正是写对的。这种写程序的方法相比一般通过测试检验程序的方法速度上要显得慢，但是通过这种方式写出来的程序往往缺陷较少，因此后期调试过程也相应比较短。除此以外，符鸿飞对算法理论和自动机理论感兴趣，并自学了计算机科学理论的基础——自动机理论。

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

　　基于硕士阶段对形式化方法的兴趣，符鸿飞通过国家公派留学找到了该领域著名学者Joost-Pieter Katoen教授，赴德国亚琛工业大学攻读形式化方法相关的博士。在攻读博士期间，符鸿飞主要研究概率系统形式化验证，并独立自主地给出了诸多相关理论问题的基础算法和计算复杂性。在博士期间，符鸿飞的研究兴趣逐渐由纯理论转向理论与应用相结合。

　　在博士后期间，符鸿飞和奥地利科学技术研究院(IST Austria)的Krishnendu Chatterjee教授合作研究概率程序的形式化验证，并发表了多篇关于基础理论的结果。程序验证(即针对程序的形式化验证)领域是理论和应用相结合的一个范例，在理论上可以开拓新的形式化方法领域，在应用上也可以和无运行时错误保证、无安全漏洞等重要的实际应用相结合。程序验证方向也和符鸿飞本科时遇到的如何保证写对程序这个问题一致。

　　面向实际，取得硕果累累

　　科研成果要运用于实际的生产和生活当中，发挥其应有的价值。这也是符鸿飞一贯以来从事科研所秉持的理念，目前，他主要研究概率程序的形式化验证，致力于能够获得一些具有实际应用背景的理论结果。

　　符鸿飞致力于理论计算机科学中的形式化方法领域。形式化方法是利用数学和逻辑的方法证明计算机系统正确性的研究领域。计算机系统的正确性在安全或任务关键系统中是一个核心课题。由于潜在的漏洞可能导致重大的人身或财产损失，如何保证关键系统不出现重大漏洞是一个重要的问题。作为理论计算机科学的一个重要分支，形式化方法为关键系统组件正确性的自动化推理和证明提供了坚实的基础，因此能够为系统是否满足一些关键的正确性性质作出最强的保证。近年来，随着系统越来越复杂，通过传统测试方法越来越难以覆盖足够多的系统执行路径。因此，形式化方法为全覆盖的、自动化的系统正确性证明提供了一个行之有效的方法。

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

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

　　截至目前，符鸿飞在理论计算机科学以及形式化方法国际著名会议以及期刊上发表论文14篇。获得过HSCC 2013最佳学生论文奖以及科学中国人2017年度人物。

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

　　在学术兼职方面，符鸿飞为国际著名学术会议和期刊ICALP、VMCAI、FOSSACS、Information and Computation, Information Processing Letters等审稿30篇左右。目前，符鸿飞在上海交通大学带领博士生进行形式化方法的深入研究，并教授《离散数学》、《程序语言理论》等与形式化方法相关的课程。同时，符鸿飞与博士导师Joost-Pieter Katoen教授、博士后合作导师Krishnendu Chatterjee教授以及国内著名学者张立军教授等保持合作关系，共同推进形式化方法的发展。

　　在团队协作方面，目前，符鸿飞主要是通过与国际国内共同研究方向的学者进行交流合作。国外主要是与奥地利科学技术研究院的博士后合作导师Krishnendu Chatterjee进行合作研究，国内主要是与上海交通大学(校内合作)、华东师范大学、中国科学院软件研究所以及北京大学等具有共同研究方向的学者进行合作交流。

　　开拓创新，自然水到渠成

　　创新是科研的灵魂，唯有通过不断创新，才有可能在研究事业中不断地披荆斩棘，勇攀高峰，符鸿飞觉得在自己这个研究领域(形式化方法)，创新可以有三种形式。

　　首先，一种创新形式是通过复杂的数学方法解决一个已经被提出的公认难题。这种形式的创新须要求研究者或研究团队有扎实的数学功底、要有一定解决数学问题的能力、同时最重要的是要对待解决的问题有充分的兴趣。比如符鸿飞获得HSCC 2013最佳学生论文奖的那篇论文，首先他对这个问题感兴趣，愿意花时间在这个问题上;其次在花时间解决这个问题的过程中，他通过持续的思考并借助自己在大学本科时期积累的数学基础解决了这个问题中两个关键的难题(连续性和无初值属性)。符鸿飞个人认为兴趣是解决这个问题的关键，否则这两个关键性难题的的解决或许会困难得多。

　　其次，创新可以通过提出新的理论概念、并通过充实的依据说明提出的概念具有理论或实际上的意义。比如符鸿飞最近几年发表在POPL、CAV以及IJCAI上的文章，都是在和合作导师交流后发现了新的理论点，随后在这些点上展开所获得的结果。目前符鸿飞正在做的几个课题也是找到了新的理论点，随后研究新的方法以解决这些新的理论问题。符鸿飞认为这种类型的创新须要对这个领域的全局有一定程度的了解。

　　再次，符鸿飞提到他研究领域中的创新还可以通过将理论结果应用到大规模工业系统中，以验证实际系统中的一些关键性质。由于符鸿飞是做理论研究的，所以在这方面还没有太多的建树。不过他提到由于理论和实际应用之间往往存在比较大的距离，因此将理论结果转化为实际应用通常需要一个多人的团队以及一两年的时间。因此完成这种类型的创新虽然理论上没什么难度，但需要一定的人力和时间。

　　最后，符鸿飞提到目前的趋势是完成创新所需的要素越来越多。除了将理论投入应用的创新需要团队和时间以外，理论性的创新也须要学术同行之间多进行交流，很多时候也须要有能力的学生对理论结果做一些初步的实验。因此，目前想完成创新须要多种要素结合在一起，在单一要素方面即使再强也难以达到好的成果。

　　面向未来，做好教学工作

　　冰冻三尺，非一日之寒。科研成果的取得也离不开一代代研究者在继承的基础上不断创新，开创新篇。良好的传承是研究事业取得大成的重要条件，所以做好教学工作与科研本身一样重要。

　　在教学方面，符鸿飞觉得首先要把学生放在首位。比如在设计教学内容的时候可以考虑什么样的内容是有助于学生的，在进行教学的时候可以先站在学生的角度看待问题、设想学生会如何去学习新的知识。学生在学习一门课程前有他们自己的知识结构，如果教师严格按照自己对课程内容的把握上课，有可能会导致学生无法将新的知识同原有的知识结构建立起联系，因此教师首先要从学生的角度出发讲课，直到学生能够循序渐进地掌握课程内容。同时，学生由于情况各不相同，在掌握课程内容方面多有差异，因此教师要对每个学生都有耐心、尽量解决每个学生的问题。

　　其次，在教学的时候，要注意调动学生的积极性、活跃课堂气氛。这样做的好处是学生的注意力会一直比较集中，同时学生也能够主动参与到课程的学习中，提高教学效果。

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

　　目前工作以及未来展望

　　目前，符鸿飞有一些关于概率程序验证的理论结果正在和合作者共同完成。关于概率程序的终止性验证，目前符鸿飞在和上海交通大学理论组合作完成几项深入的研究;关于概率程序资源消耗的验证，符鸿飞目前正在带领上海交通大学理论组的一个学生进行研究;而关于概率程序的灵敏性验证，符鸿飞也正与华东师范大学的合作者共同开展研究。另外，符鸿飞也在和中国科学院软件研究所以及北京大学的一些研究人员讨论合作事宜。

　　展望未来，符鸿飞的一个短期的憧憬是希望这些结果都能够圆满完成，并且能被学术界认可。长远来看，他希望作出一些能够应用在工业界关键场合的成果。我们相信，经过坚持不懈的积极开拓，假以时日，他一定能得偿所愿。