兴趣，求学路上的动力
20世纪70年代后期，随着一篇著名报告文学《哥德巴赫猜想》的发表，数学家陈景润的事迹影响和带动了一代青年人走上数学研究的道路。作为标准的“80后”，符鸿飞同样受此热潮，对于数学表现出不一样的兴趣和天赋，常常一头扎进数学课程的学习中，在数学世界里寻找乐趣。
数学作为一种纯粹的思维形式，对很多人而言，似乎总和枯燥、乏味脱不开关系。但在符鸿飞的认知中，他却总能揭开数学那一层神秘的面纱，感受到这门学问的纯净和美。
“万物皆数”——古希腊数学家毕达哥拉斯的这句话固然过于夸张，但符鸿飞始终相信，数学的魅力就在于它的抽象理论应用能够揭示各种现象和问题的本质，让人们发现这个世界的精彩。
像所有的“80后”科学家一样，通常在给他们打标签的时候，用“热情”“自信”“勇于尝试”这三个词来形容他们准没错。符鸿飞除此之外，还要加上一个特性——“耐烦”。
他似乎具有不属于这个年龄段的耐心和沉稳。“数学是理工学科的基础，在支撑其他理工学科的同时也为自身的发展提供必要的工具。”符鸿飞说道，“和人们的想象不同，数学的成分并不是完全在于计算，它更需要严谨的证明来确立结论，也需要对数学理论和现象的深刻理解。数学因反映客观真理、不以人的意志为转移而独具魅力。”
进入90年代之后，计算机开始普及，逐步进入千家万户，符鸿飞成为那个年代最早接触个人计算机的一批人。在符鸿飞看来，在计算机领域若要有突破必须得先在理论上有所创新，而理论计算机科学领域相当依赖数学。反过来，计算机科学中的问题也日渐成为数学发展的一个重要源泉。另外也值得一提的是，日渐强大的计算机也为解决各种数学难题提供了便利。
正是为了探索与数学有一定联系的计算机问题，符鸿飞于2003年考入上海交通大学计算机科学与技术专业。在本科求学期间，在编写程序的过程中，符鸿飞对如何保证程序编写的正确性产生了困惑，因此在写完程序后往往会反复读几遍，确保程序真正是写对的。这种写程序的方法相比一般通过测试检验程序的方法速度上要显得慢，但是通过这种方式写出的程序往往缺陷更少，因此后期调试过程也相应更短。
真正把符鸿飞带入形式化方法研究之路的是上海交通大学的傅育熙教授。在硕士研究生阶段，符鸿飞选择傅教授作为自己的导师，傅育熙的研究方向是理论计算机科学中的进程理论。在那段日子里，符鸿飞一直“潜”在计算机科学的理论世界里，探求更多的奥秘。在导师的指导下，符鸿飞对一些无穷状态进程模型的可判定性和计算复杂性进行了研究，并在互模拟判定及模型检测算法方面做出了理论上的贡献，为后续的研究打下了坚实的基础。这一阶段的求学经历让符鸿飞对利用数学方法证明系统正确性的形式化方法领域产生了浓厚兴趣。
接下来，符鸿飞通过国家公派留学赴德国亚琛工业大学（RWTH Aachen）攻读形式化方法的博士学业。亚琛工业大学是德国最负盛名的理工科大学之一，来自五洲四海的莘莘学子聚集于此。亚琛工业大学理工科实力强劲，电子、机械制造方面的排名一直名列德国第一，计算机、物理等学科也在德国大学排行榜上位列三甲。这一留学经历使符鸿飞亲身体会到了不同的科研文化，让他大开眼界，呼吸到了很多与国内截然不同的新鲜空气。比如他在德国接触到了形式化方法的理论前沿，了解许多数学及数理逻辑方面之前从未接触过的方法和概念。同时，他在德国也体会到了平等、宽松而严谨的科研环境，比如重论文质量而非论文数量，但同时导师对论文要求也很严格等。
在亚琛工业大学，面对面向国际大师们（如该领域著名学者Joost-Pieter Katoen教授等）学习的机会，使得符鸿飞逐渐具备了极高的国际视野，与国际著名的研究中心保持着密切的合作关系，从而对国际主流发展方向有了更准确的把握。在博士后期间，符鸿飞与奥地利科学技术研究院（IST Austria）著名学者Krishnendu Chatterjee教授合作研究概率程序的形式化验证，并发表了多篇关于基础理论的成果。
热爱，科研奋进的初心
受益于当今互联网和计算机新一代技术的创新，无处不在的大数据、强大的运算能力以及深度学习模式的突破，使人工智能驶入了高速发展的快车道。这一轮热潮势不可挡，机器学习、人工神经网络等新名词成为热门词汇。而对于符鸿飞致力于研究的理论计算机科学中的形式化方法，则被业内很多人视为冷门，甚至被年轻学子们称为“坑”。
究其原因，不仅是因为这一领域的逻辑推演过于严格、思维太过抽象，而且需要长时间深入的思考、反复学习才可能有所得。这是一个漫长的、循序渐进的过程。在符鸿飞看来，“无论是人工智能还是量子通信，都需要数学、物理、计算机等基础学科作有力支撑。我们之所以缺乏重大原创性科研成果，‘卡脖子’就卡在这些基础学科上。”所以他“欣然入坑”，板凳甘坐十年冷。
符鸿飞说道，在理论计算机科学领域，形式化方法是利用数学和逻辑的方法证明计算机系统正确性的研究领域。形式化方法在20世纪60年代被提出，经过多年的研究，到目前为止诸如抽象解释、模型检测、定理证明等方法技术日臻成熟，并被应用于高可靠编译器、云计算、操作系统中，保证这些安全或应用关键系统的正确性。
目前，电子计算机技术和以其为基础的互联网科技正深刻改变着人类的生产和生活。与此同时，计算机和互联网的效率和安全问题也成为摆在人们面前的一项重要课题。由于潜在的漏洞可能导致重大的人身或财产损失，如何保证关键系统不出现重大漏洞是一个重要的问题。作为理论计算机科学的一个重要分支，形式化方法为关键系统组件正确性的自动化推理和证明提供了坚实的基础，因此能够为系统是否满足一些关键的正确性性质作出强有力的保证。近年来，随着系统越来越复杂，通过传统测试方法越来越难以覆盖足够多的系统执行路径。因此，形式化方法为全覆盖的、自动化的系统正确性证明提供了一个行之有效的方法。
在符鸿飞眼中，计算机、数学、推理、验证、不仅是工具，更是一种文化，这种文化鞭策我们要有一种要勇往直前的探索精神。钻研新理论、掌握新技术，要善于领悟，更要敢于创新。符鸿飞说，做科研的过程就如同小马过河一样，你问再多的人，那都是别人的感受，谁都不能代替你作出判断。如果不亲自去尝试、去突破，就永远不知道这条道路的下一站是什么风景。十多年来，符鸿飞就这样一直在这一领域脚踏实地前行着，日积月累地钻研与创新着。
符鸿飞在形式化方法中的两个重要方向——模型检测和程序验证中都有突出贡献。模型检测是研究如何验证系统模型正确性的方向。在模型检测方面，符鸿飞着力研究概率模型检测的算法、可判定性和计算复杂性，并获得了一些基础性理论成果，发表在著名理论计算机科学学术会议ICALP、FOSSACS、HSCC、FSTTCS等上。相对于模型检测，程序验证是研究如何验证程序正确性的方向。在程序验证方面，符鸿飞在程序终止性及运行时间验证方面也取得了诸多基础性理论结果，并发表在国际顶级形式化方法、程序语言理论及人工智能学术会议POPL、CAV、IJCAI上。
坚守，通往未来的希望
在做科研的同时，符鸿飞还担任着上海交通大学电子信息与电气工程学院本科生和研究生的教学工作。他把人才培养看作是学科长远发展的一个重要内容。学科未来的发展要靠年轻一代，要有一批杰出的学科带头人，这样才能为今后开展原创性工作、深度研究提供保障。
或许是因为年龄差距不大的缘故，符鸿飞和他的学生们相处总是特别融洽，完全没有代沟，可谓亦师亦友。“我觉得最重要的是要换位思考。”他强调道，“比如在设计教学内容时可以考虑什么样的内容是有助于学生的，在进行教学时可以先站在学生的角度看待问题、设想学生会如何去学习新的知识。学生在学习一门课程前有其知识结构，如果教师严格按照自己对课程内容的把握去上课，有可能会导致学生无法将新的知识同原有的知识结构建立起联系，因此教师首先要从学生的角度出发去讲课，直到学生能够循序渐进地掌握课程内容。”同时，由于学生情况各不相同，在掌握课程内容方面多有差异，因此符鸿飞认为，作为老师要学会因材施教，因势施教，激发出他们的兴趣，找出他们的特长，对不同类型的学生，要进行分类培养。
认真、严谨的敬业精神是科技工作者的基本素养；勤学好问、刻苦钻研是做好研究工作的基础；勤于思考、集思广益、锲而不舍是科研的灵魂；诚信待人、合作共赢是解决问题的康庄大道。这种坚定的理念被符鸿飞自然而然地贯穿在教学过程中，灌输给新一代年轻人，让他们受益匪浅。
正如德国数学家克莱因曾说的：“如阿基米德、牛顿与高斯这样伟大的数学家，总是不偏不倚地把理论与应用结合起来。”一切科学终将为解决实际问题而服务，为人类社会的进步而服务。这一点，符鸿飞深以为然，铭记于心，并时刻践行着。虽然长期致力于形式化方法的理论研究事业，但他着重于理论联系实际，尽量将理论成果应用于现实生产生活中，发挥他们应有的价值。
长期以来，符鸿飞与博士导师Joost-Pieter Katoen教授、博士后合作导师Krishnendu Chatterjee教授等业界大师保持合作关系，共同推进形式化方法的发展。目前，符鸿飞有一些关于概率程序验证的理论结果正在与合作者共同完成。关于概率程序的终止性和资源消耗的验证，他正与上海交通大学BASICS实验室理论组合作完成几项深入的研究；而关于概率程序的灵敏性验证，他目前也正与华东师范大学的合作者共同开展研究。
“如切如磋，如琢如磨”“虽千万人吾往矣”，这就是符鸿飞，在他身上，你能读到那种纯粹的科学家的科研精神，一种为了理想而不避风雨勇往直前的热忱。他就是形式化方法研究路上的一位自由探索者，以学问为矛、以理想为马，自由驰骋，风雨兼程，在科研领域里开辟出一条宽阔的道路。
