鑄就理論基石 驗證系統邏輯
——記上海交通大學電子信息與電氣工程學院特別副研究員符鴻飛

□ 黃 健

“實踐是檢驗真理的唯一標準”，很多軟件、系統在開發時都會進行模擬驗證，以確保順利運行。然而近些年來，模擬驗證的短板逐漸凸顯——伴隨著計算機的飛速發展，越來越多超大規模設計出現，對于這些設計來說，仿真挑戰過于耗費時間，從理論上進行測試反而更為合適。這種測試被稱為“形式化驗證”，是一種窮盡式數學技術，其原理是利用數學和邏輯的方法來證明計算機系統的正確性。

在移動互聯網深刻影響著人類生產生活的今天，保障計算機的安全性至關重要，而這其中的核心課題就是確保計算機系統的正確性。由于潛在的漏洞可能導致重大的人身或財產損失，因此，如何保證關鍵系統不出現重大漏洞是一個重要的問題。作為理論計算機科學的一個重要分支，形式化驗證為關鍵系統組件正確性的自動化推理和證明提供了堅實的基礎，因此能夠為系統是否滿足一些關鍵的正確性質作出最強的保證。上海交通大學電子信息與電氣工程學院特別副研究員符鴻飛長期致力于理論計算機科學中的形式化驗證領域，在取得一系列原創性理論成果的同時，他不忘尋求與工業界實際相結合，在理論成果付諸應用的道路上展開了諸多探索。

“熱愛是最好的老師”

愛因斯坦曾經說過：“我認為對于一切情況，只有熱愛才是最好的老師。”相比于其他外在原因，“熱愛”這一內在動力往往更為持久有效。自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教授及國內一些著名學者保持合作關系，共同推進形式化方法的發展。

尋求應用 教學傳承

毋庸置疑，形式化驗證是一個偏理論的研究方向，但最近幾年，它在工業界的應用越來越多。“編譯器的驗證、防止黑客入侵、保障云計算的安全，這些都離不開形式化驗證。”符鴻飛對此如數家珍。

2016年在羅馬

所謂編譯器，就是將“一種語言（通常為高級語言）”翻譯為“另一種語言（通常為低級語言）”的程序，簡單來說就是把寫好的代碼轉化成直接可執行的二進制文件。編譯器是一個比較關鍵的系統軟件，如果它出錯的話，那么通過這個編譯器所編譯的二進制的文件都可能有問題，因此，運用形式化方法保障其正確性至關重要。

對于操作系統而言，防止外部傷害如黑客入侵是必須要考慮的關鍵點。一般來說，黑客想要入侵操作系統，就必須要攻擊程序員在寫程序的時候沒有考慮到的漏洞。而通過形式化方法，可以交由計算機去檢查漏洞，如果最終通過定理證明的方法證明了操作系統沒有漏洞的話，就可以說這個操作系統在形式化驗證的正確性定義下是安全的。“這方面目前已經做出了相關的操作系統，并且成功通過了黑客的攻擊測試。”

形式化驗證的應用還體現在備受矚目的云計算技術上。毫無疑問，云計算是21世紀到目前為止最成功的技術之一，對于任何規模的企業都能提供不同程度的幫助。正因為此，通過形式化方法排除系統的錯漏尤為重要。

或許有人會覺得，理論研究是一項與實際相距甚遠的工作，大多是空中樓閣。但符鴻飛不這么想，他堅決反對將理論研究與實際工作割裂開來。他認為，或許某些理論在誕生之初恍若不可實現，但隨著科學研究的深入發展和科學技術的不斷進步，有朝一日它們或許可以發揮出各自的作用，甚至直接指導實踐。正因為此，符鴻飛一直主張從事理論研究的人應該對其所在領域的應用情況做一定了解，尤其是計算機專業。“在計算機專業從事理論研究與在數學、物理等專業是不一樣的，后者可以做一些很純粹的理論研究，而計算機專業則需要關注工業界的發展，以期早日與實踐接軌。”他說。

博士畢業照

作為青年科學家，符鴻飛很慶幸選擇了上海交通大學，加入了John Hopcroft中心和BASICS實驗室。為了加快培育青年學者，學校有著良好的學術氛圍，讓他能夠心無旁騖地從事科研和教學工作。

在教學方面，符鴻飛認為要把學生放在首位。如在設計教學內容的時候，應該考慮什么樣的內容是對學生有幫助的，在進行教學的時候可以先站在學生的角度看待問題，設想學生會如何去學習新的知識。“學生在學習一門課程前有他們自己的知識結構，如果教師嚴格按照自己對課程內容的把握上課，有可能會導致學生無法將新的知識同原有的知識結構建立起聯系，因此教師首先要從學生的角度出發講課，直到學生能夠循序漸進地掌握課程內容。”符鴻飛說。同時，由于學生的情況各不相同，在掌握課程內容方面多有差異，因此教師要對每個學生都有耐心，盡量解決每個學生的問題。另外，在教學的時候，應注意調動學生的積極性、活躍課堂氣氛。這樣做的好處是學生的注意力會一直比較集中，同時學生也能夠主動參與到課程的學習中，提高教學效果。最后，在課程內容的設置方面要聯系整個專業背景，力求學生在修習過課程后能夠更好地適應專業發展趨勢。講課時要注意保持講課邏輯的一致性和內在關聯性，使得學生能夠融會貫通，還要隨時觀察學生掌握課程內容的情況并進行有必要的干預。

科學研究最重要的就是傳承，科研成果的取得離不開一代代研究者在繼承的基礎上加以創新。符鴻飛希望通過自己的教學，盡快培養出具有扎實專業背景、能夠自主開展科研工作的學生，共同探索如何將所創理論應用于實踐。

從事理論研究是一項孤獨的工作，截至目前，符鴻飛的絕大多數成果都是自己獨立完成的。盡管如此，他依然對這個研究方向保持著濃厚的興趣。在他看來，研究工作的意義就是他的動力。“只要想到能夠用自身所學做出貢獻，所有獨行的孤寂和壓力就都得到了慰藉。”他說。