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

　　□　黄 健
　　

　　
　　“实践是检验真理的唯一标准”，很多软件、系统在开发时都会进行模拟验证，以确保顺利运行。然而近些年来，模拟验证的短板逐渐凸显——伴随着计算机的飞速发展，越来越多超大规模设计出现，对于这些设计来说，仿真挑战过于耗费时间，从理论上进行测试反而更为合适。这种测试被称为“形式化验证”，是一种穷尽式数学技术，其原理是利用数学和逻辑的方法来证明计算机系统的正确性。
　　在移动互联网深刻影响着人类生产生活的今天，保障计算机的安全性至关重要，而这其中的核心课题就是确保计算机系统的正确性。由于潜在的漏洞可能导致重大的人身或财产损失，因此，如何保证关键系统不出现重大漏洞是一个重要的问题。作为理论计算机科学的一个重要分支，形式化验证为关键系统组件正确性的自动化推理和证明提供了坚实的基础，因此能够为系统是否满足一些关键的正确性质作出最强的保证。上海交通大学电子信息与电气工程学院特别副研究员符鸿飞长期致力于理论计算机科学中的形式化验证领域，在取得一系列原创性理论成果的同时，他不忘寻求与工业界实际相结合，在理论成果付诸应用的道路上展开了诸多探索。
　　

“热爱是最好的老师”

　　爱因斯坦曾经说过：“我认为对于一切情况，只有热爱才是最好的老师。”相比于其他外在原因，“热爱”这一内在动力往往更为持久有效。自2003年考入上海交通大学计算机科学与技术专业以来，符鸿飞一直对其专业领域保持着浓厚的兴趣，心无旁骛地投身其中。
　　回想起进入形式化研究领域的原因，符鸿飞表示，在本科求学期间，他经常编写程序，这是计算机专业学生的日常，但与别人不同的是，符鸿飞没有止步于编程。在这个过程中，他对如何保证程序编写的正确性产生了困惑，因此在写完程序后往往会反复读几遍以确保其正确性。这样写程序的速度很慢，因此，符鸿飞萌生了学习如何对程序进行快速验证的念头。
　　就这样，在上海交通大学读研期间，符鸿飞选择了研究理论计算机科学中进程理论的傅育熙教授作为自己的导师。在他的指导下，符鸿飞对一些无穷状态进程模型的可判定性和计算复杂性进行了研究，并在互模拟判定及模型检测算法方面做出了理论上的贡献。正是硕士阶段的求学经历让符鸿飞对利用数学方法证明系统正确性的形式化方法领域产生了兴趣。
　　学习的乐趣就是不断发现新的感兴趣的研究方向，从而不断开辟新的研究领域。对形式化方法产生兴趣之后，符鸿飞通过国家公派留学机会找到了该领域著名学者Joost-Pieter Katoen教授，赴德国亚琛工业大学计算机科学系攻读形式化方法相关的博士。读博期间，符鸿飞主要研究概率系统形式化验证，并独立自主地给出了诸多相关理论问题的基础算法和计算复杂性。花费4年时间顺利拿到博士学位之后，符鸿飞开展了博士后研究，和奥地利科学技术研究院（IST Austria）的Krishnendu Chatterjee教授合作研究概率程序的形式化验证，并发表了多篇关于基础理论的结果。
　　尽管在国外学习工作多年，但符鸿飞的心中始终记挂着祖国和故乡。他期盼着能回到母校，在求学多年的环境中，与敬爱的师长共事。念念不忘，必有回响。2017年，他成功加入上海交通大学电子信息与电气工程学院，任特别副研究员，一圆心中夙愿。
　　

创立形式化验证新成果

　　多年来，符鸿飞埋首形式化验证领域，不懈钻研。从广义上讲，形式化方法是借助数学的方法来解决软件工程领域的问题，主要包括建立精确的数学模型及对模型的分析活动。狭义地讲，它就是运用形式化语言，进行形式化的规格描述、模型推理和验证的方法。近年来，随着系统越来越复杂，通过传统测试方法越来越难以覆盖足够多的系统执行路径。因此，形式化方法为全覆盖、自动化的系统正确性证明提供了一个行之有效的方法。
　　形式化方法研究有两个重要方向，即模型检测和程序验证，符鸿飞在这两个领域都取得了原创性成果。
　　模型检测是研究如何验证系统模型正确性的研究领域。“简单来说，就是通过数学建模去证明系统模型具有哪些性质。”符鸿飞解释道。在这方面，他着力研究概率模型检测的算法、可判定性和复杂性，并获得了一些基础性理论成果。在模型检测算法方面，符鸿飞以独立作者身份给出了关于连续时间马尔可夫过程时序逻辑的两个基础模型检测算法，并发表在国际著名形式化验证学术会议FOSSACS、HSCC上。其中，发表在HSCC上的论文获得了2013年度最佳学生论文奖。在可判定性和计算复杂性理论方面，他着力研究离散时间马尔可夫过程上关于互模拟等价关系的可判定性和计算复杂性，并以独立作者或主要贡献者身份在国际著名理论计算机科学学术会议ICALP、FSTTCS上发表多篇重要论文。
　　相对于模型检测，程序验证是直接针对程序代码的，就是研究如何验证程序代码正确性的方向。在程序验证方面，符鸿飞在程序终止性及运行时间验证方面取得诸多基础性理论结果，并发表在国际顶级形式化方法、人工智能及程序语言学术会议POPL、CAV、IJCAI上。首先，他作为主要贡献者与合作者提出了分级上鞅在同时带有恶意非确定性与友善非确定性概率程序上的定义，并给出了线性分级上鞅的合成算法以及相关的计算复杂性，进而为带有非确定性的概率程序终止性与期望运行时间验证提供了一个坚实的理论基础；同时，他也证明了分级上鞅可以导出有限步内不终止概率的指数衰减性。
　　其次，符鸿飞通过实代数几何中的一些数学定理及半正定规划给出了概率程序上合成多项式分级上鞅的一个高效算法。
　　再次，他将分级函数推广至非概率递归程序，进而通过线性规划以及实代数几何上的一些定理给出了一个输出非概率递归程序精确运行时间的验证算法；该算法可以有效地输出很多经典递归算法（如归并排序、最近点对算法等）的精确非多项式运行时间。
　　最后，他基于一元递归关系针对随机递归算法给出了一个验证精确期望运行时间的高效算法，该算法可以在线性时间内输出一个由随机递归算法导出的递归关系的精确期望运行时间。截至目前，符鸿飞已在理论计算机科学、形式化方法国际著名会议及期刊上发表论文14篇。
　　尽管已经取得了许多成绩，但他没有自满，而是在已经取得成果的基础上不断展开新的探索。2016年，他参与了一项国家自然科学基金重点项目“大规模概率并发实时系统模型检验”。该项目的重点在于研究新的理论方法以有效验证兼具随机性、并发性及实时性特征的大规模系统。随机性、并发性及实时性都是难以通过直觉或是大规模测试保证正确性的复杂系统性质。通过该项目的研究，能够在为保证大规模概率并发实时系统关键性质方面给出一个有效的理论框架。
　　除了自身的科研工作，符鸿飞还积极承担学术兼职，为理论计算机科学国际著名学术会议和期刊ICALP、VMCAI、FOSSACS、Information and Computation、Information Processing Letter等审稿30余篇。目前，他在上海交通大学带领博士生和硕士生进行形式化方法的研究，并教授“程序语言理论”“离散数学”等和形式化方法相关的课程。同时，他还与博士导师Joost-Pieter Katoen教授、博士后合作导师Krishnendu Chatterjee教授及国内一些著名学者保持合作关系，共同推进形式化方法的发展。
　　

寻求应用 教学传承

　　毋庸置疑，形式化验证是一个偏理论的研究方向，但最近几年，它在工业界的应用越来越多。“编译器的验证、防止黑客入侵、保障云计算的安全，这些都离不开形式化验证。”符鸿飞对此如数家珍。
　　所谓编译器，就是将“一种语言（通常为高级语言）”翻译为“另一种语言（通常为低级语言）”的程序，简单来说就是把写好的代码转化成直接可执行的二进制文件。编译器是一个比较关键的系统软件，如果它出错的话，那么通过这个编译器所编译的二进制的文件都可能有问题，因此，运用形式化方法保障其正确性至关重要。
　　对于操作系统而言，防止外部伤害如黑客入侵是必须要考虑的关键点。一般来说，黑客想要入侵操作系统，就必须要攻击程序员在写程序的时候没有考虑到的漏洞。而通过形式化方法，可以交由计算机去检查漏洞，如果最终通过定理证明的方法证明了操作系统没有漏洞的话，就可以说这个操作系统在形式化验证的正确性定义下是安全的。“这方面目前已经做出了相关的操作系统，并且成功通过了黑客的攻击测试。”
　　形式化验证的应用还体现在备受瞩目的云计算技术上。毫无疑问，云计算是21世纪到目前为止最成功的技术之一，对于任何规模的企业都能提供不同程度的帮助。正因为此，通过形式化方法排除系统的错漏尤为重要。
　　或许有人会觉得，理论研究是一项与实际相距甚远的工作，大多是空中楼阁。但符鸿飞不这么想，他坚决反对将理论研究与实际工作割裂开来。他认为，或许某些理论在诞生之初恍若不可实现，但随着科学研究的深入发展和科学技术的不断进步，有朝一日它们或许可以发挥出各自的作用，甚至直接指导实践。正因为此，符鸿飞一直主张从事理论研究的人应该对其所在领域的应用情况做一定了解，尤其是计算机专业。“在计算机专业从事理论研究与在数学、物理等专业是不一样的，后者可以做一些很纯粹的理论研究，而计算机专业则需要关注工业界的发展，以期早日与实践接轨。”他说。
　　作为青年科学家，符鸿飞很庆幸选择了上海交通大学，加入了John Hopcroft中心和BASICS实验室。为了加快培育青年学者，学校有着良好的学术氛围，让他能够心无旁骛地从事科研和教学工作。
　　在教学方面，符鸿飞认为要把学生放在首位。如在设计教学内容的时候，应该考虑什么样的内容是对学生有帮助的，在进行教学的时候可以先站在学生的角度看待问题，设想学生会如何去学习新的知识。“学生在学习一门课程前有他们自己的知识结构，如果教师严格按照自己对课程内容的把握上课，有可能会导致学生无法将新的知识同原有的知识结构建立起联系，因此教师首先要从学生的角度出发讲课，直到学生能够循序渐进地掌握课程内容。”符鸿飞说。同时，由于学生的情况各不相同，在掌握课程内容方面多有差异，因此教师要对每个学生都有耐心，尽量解决每个学生的问题。另外，在教学的时候，应注意调动学生的积极性、活跃课堂气氛。这样做的好处是学生的注意力会一直比较集中，同时学生也能够主动参与到课程的学习中，提高教学效果。最后，在课程内容的设置方面要联系整个专业背景，力求学生在修习过课程后能够更好地适应专业发展趋势。讲课时要注意保持讲课逻辑的一致性和内在关联性，使得学生能够融会贯通，还要随时观察学生掌握课程内容的情况并进行有必要的干预。
　　科学研究最重要的就是传承，科研成果的取得离不开一代代研究者在继承的基础上加以创新。符鸿飞希望通过自己的教学，尽快培养出具有扎实专业背景、能够自主开展科研工作的学生，共同探索如何将所创理论应用于实践。
　　从事理论研究是一项孤独的工作，截至目前，符鸿飞的绝大多数成果都是自己独立完成的。尽管如此，他依然对这个研究方向保持着浓厚的兴趣。在他看来，研究工作的意义就是他的动力。“只要想到能够用自身所学做出贡献，所有独行的孤寂和压力就都得到了慰藉。”他说。
　　
　　
　　　　
专家简介：
　　
　　符鸿飞，上海交通大学电子信息与电气工程学院特别副研究员，兼任CCF形式化方法专委会委员。2003年考入上海交通大学计算机科学与技术专业，2014年取得德国亚琛工业大学计算机科学系博士学位。他长期致力于探索理论计算机科学中形式化方法领域的理论问题，在形式化方法的两个重要方向——模型检测和程序验证中都有突出贡献。迄今为止，在理论计算机科学、形式化方法国际著名学术会议及期刊上以主要贡献者身份发表论文10余篇，为ICALP、VMCAI、FOSSACS、Information and Computation、Information Processing Letter等审稿30余篇。参与国家自然科学基金重点项目1项，获得国家自然科学青年基金资助1项，曾获HSCC 2013年度最佳学生论文奖。