扎實打根基 創(chuàng)新展宏圖
——記上海交通大學電子信息與電氣工程學院特別副研究員符鴻飛

◎ 文/曹 莉

他對科研的態(tài)度是嚴謹治學、打牢根基。他創(chuàng)新的 “形式化驗證”是一種從理論上進行測試的全新方法，被形象地稱作為 “窮盡式數學技術”，其原理是利用數學和邏輯的方法來證明計算機系統(tǒng)的正確性。

他長期致力于理論計算機科學中的形式化驗證領域研究，在獲得一系列原創(chuàng)性理論成果的同時，緊密結合工業(yè)界生產實際，致力于把理論成果成功地轉化為工業(yè)實踐，并取得了豐碩的成果。

他的學術成就豐富，在理論計算機科學、形式化方法國際著名學術會議及期刊上以主要貢獻者身份發(fā)表論文14篇，為ICALP、VMCAI、FOSSACS、Information and Computation、Information Processing Letter等審稿30余篇，參與國家自然科學基金重點項目1項，獲得國家自然科學青年基金資助1項，曾獲HSCC 2013年度最佳學生論文獎以及科學中國人2017年度人物。

他就是上海交通大學電子信息與電氣工程學院特別副研究員符鴻飛。

熱愛專業(yè)領域,邁向縱深地帶

作為學者，符鴻飛是個愛學習愛鉆研的人。任何一門學科，任何一個專業(yè)要想深入學習了解，真正掌握其中的奧秘，就必須有無比熱愛的胸懷和敢于向縱深地帶不斷探索前進的精神。符鴻飛的身上具有這種科研的精神特質，這種特質來自于他對專業(yè)領域不斷學習、研究和攻關。

當他回憶起自己的成長之路時，心情一如陽光那般燦爛。2003年，他考入上海交通大學計算機科學與技術專業(yè)。他說：“當時之所以會選擇計算機專業(yè)是因為想探索與數學有一定聯系的計算機問題?！彼宄赜浀米约涸谧x本科期間對如何保證程序編寫的正確性產生過困惑，因此在寫完程序后往往會反復讀幾遍程序，確保程序不會出錯。而這種寫程序的方法與通常測試檢驗程序的方法相比速度比較慢，但通過這種寫程序的方法又有缺陷較少的優(yōu)點，使后期調試過程變得相應較短。他興奮于自己的研究發(fā)現，加速了他向形式化驗證這個縱深領域邁進的步伐。

符鴻飛真正對利用數學方法證明系統(tǒng)正確性的形式化驗證領域產生濃厚興趣的是在他碩士研究生階段。攻讀研究生期間，他選擇了上海交通大學傅育熙教授作為自己的導師。傅教授的研究方向是理論計算機科學中的進程理論。正是在傅教授的指導下，符鴻飛對一些無窮狀態(tài)進程模型的可判定性和計算復雜性進行了全面系統(tǒng)的研究，并在互模擬判定以及模型檢測算法方面作出了理論上的貢獻。

學習最大的樂趣就是不斷有新發(fā)現新方向，從而不斷挺進縱深研究地帶。為把形式化驗證學透搞通，形成形式化驗證的一套方法體系，他通過國家公派留學找到了該領域著名學者Joost-Pieter Katoen教授，赴德國亞琛工業(yè)大學攻讀與形式化驗證相關的博士。期間，他重點研究了概率系統(tǒng)形式化驗證，獨自給出了諸多相關理論問題的基礎算法和計算復雜性，并逐漸由純理論轉向理論與應用相結合。在花費4年時間攻讀完博士并拿到學位后，符鴻飛又踏上了博士后研究的征程，與奧地利科學技術研究院（IST Austria） 的Krishnendu Chatterjee教授合作研究概率程序的形式化驗證，并發(fā)表了多篇關于基礎理論的結果。

隨著嚴謹求學的不斷深入，他逐漸形成了一個觀點，那就是程序驗證（即針對程序的形式化驗證）領域是理論和應用相結合的一個范例，在理論上可以開拓新的形式化驗證領域，在應用上也可以和無運行時錯誤保證、無安全漏洞等重要的實際應用相結合。而程序驗證方向也同他本科時遇到的如何保證寫對程序這個問題高度一致。這令他甚感欣慰。

2017年，他帶著回報祖國、感恩母校的情懷從國外歸來，一如自己所愿，成為上海交通大學電子信息與電氣工程學院集體的一分子，并任特別副研究員，這讓他倍感榮幸與快樂。在此，他開始新的科研跋涉之旅，但他不問艱辛只管耕耘。

創(chuàng)新關鍵成果,推進科學發(fā)展

計算機系統(tǒng)的正確性在安全或任務關鍵系統(tǒng)中是一個核心課題。由于潛在的漏洞可能導致重大的人生或財產損失，如何保證關鍵系統(tǒng)不出現重大漏洞是一個重要的問題。

近年來，隨著計算機系統(tǒng)越來越復雜，通過傳統(tǒng)測試方法越來越難以覆蓋足夠多的系統(tǒng)執(zhí)行路徑。因此，致力于理論計算機科學中的形式化驗證領域研究的符鴻飛利用數學和邏輯的方法來證明計算機系統(tǒng)研究領域的正確性，在理論背景和實際應用成果上可知，形式化驗證為全覆蓋的、自動化的系統(tǒng)正確性證明提供了一個行之有效的方法。作為理論計算機科學的一個重要分支，形式化驗證為關鍵系統(tǒng)組件正確性的自動化推理和證明提供了堅實的基礎，因此能夠為系統(tǒng)是否滿足一些關鍵的正確性性質作出了可靠保證。

形式化驗證中的模型檢測和程序驗證是他研究的兩個重要方向，他付出了很多心血，做出了重大貢獻。說起模型檢測問題，其實就是研究如何驗證系統(tǒng)模型正確性的研究領域。他著力研究概率模型檢測的算法、可判定性和計算復雜性，并獲得了一些基礎性理論成果。在模型檢測算法上，他以獨立作者身份給出了關于連續(xù)時間馬爾可夫過程時序邏輯的兩個基礎模型檢測算法，并發(fā)表在國際著名形式化驗證學術會議FOSSACS、HSCC上。其中發(fā)表在HSCC上的論文獲得了最佳學生論文獎。在可判定性和計算復雜性理論方面，他著力研究離散時間馬爾可夫過程上關于互模擬等價關系的可判定性和計算復雜性，并以獨立作者或主要貢獻者身份在國際著名理論計算機科學學術會議ICALP、FSTTCS上發(fā)表多篇重要論文。

相對于模型檢測，程序驗證是研究如何驗證程序正確性的方向。關于程序驗證問題，他在程序終止性以及運行時間驗證方面取得諸多基礎性理論成果，并發(fā)表在國際頂級形式化方法、程序語言理論以及人工智能學術會議POPL、CAV、IJCAI上。他作為主要貢獻者與合作者提出了分級上鞅在同時帶有惡意非確定性與友善非確定性概率程序上的定義，并給出了線性分級上鞅的合成算法以及相關的計算復雜性，進而為帶有非確定性的概率程序終止性與期望運行時間驗證提供了一個堅實的理論基礎；同時，他在該成果中證明了分級上鞅可以導出有限步內不終止概率的指數衰減性（POPL 2016，TOPLAS 2018）。他通過實代數幾何中的一些數學定理以及半正定規(guī)劃給出了概率程序上合成多項式分級上鞅的一個高效算法（CAV 2016）。他針對概率程序的資源消耗給出了一個基礎的驗證算法（IJCAI 2018）。最后，他將分級函數推廣至非概率遞歸程序，進而通過線性規(guī)劃以及實代數幾何上的一些定理給出了一個輸出非概率遞歸程序精確運行時間的驗證算法；該算法可以有效地輸出很多經典遞歸算法（如歸并排序、最近點對算法等）的精確非多項式運行時間 (CAV 2017)；同時，他基于一元遞歸關系針對隨機遞歸算法給出了一個驗證精確期望運行時間的高效算法；該算法可以在線性時間內輸出一個由隨機遞歸算法導出的遞歸關系的精確期望運行時間（CAV 2017）。

創(chuàng)新是科研的靈魂。符鴻飛覺得在形式化驗證這個研究領域的創(chuàng)新有三種成果：一是通過復雜的數學方法解決一個已經被提出的公認難題；二是創(chuàng)新可以通過提出新的理論概念、并通過充實的依據說明提出的概念具有理論或實際上的意義；三是創(chuàng)新還可以通過將理論成果應用到大規(guī)模工業(yè)系統(tǒng)中，以驗證實際系統(tǒng)中的一些關鍵性質。

作為導師，他在上海交通大學帶領博士生進行形式化方法深入研究，并教授《離散數學》、《程序語言理論》等與形式化驗證相關的課程。同時，他與博士導師Joost-Pieter Katoen教授、博士后合作導師Krishnendu Chatterjee教授以及一些國內著名學者保持合作關系，致力于推進形式化驗證的更大發(fā)展。

對從事教學與科研的專家來說，科學研究最重要的就是傳承，科研成果的取得需要一代代科研人在承上啟下中再創(chuàng)新高。符鴻飛真切地希望通過自己悉心傳教，盡早培養(yǎng)出一批具有扎實專業(yè)知識基礎、能夠獨立自主開展科研工作的學生，進一步探索如何將所創(chuàng)理論更多地應用于豐富的實踐中，推動學科專業(yè)邁向科學的頂峰。