4月22日，應計算機科學國家重點實驗室邀請，美國哈佛大學工程和應用科學學院Greg Morrisett 教授訪問軟件所并進行學術交流，并作了題為An Algebraic Regular Parser Generator的學術報告，報告會由林惠民院士主持。 

眾所周知，大多數軟件故障隔離技術依賴于對機器代碼的分析，Greg Morrisett教授與其團隊的研究卻發現，現有的針對x86架構的機器代碼分析工具存在錯誤且效率較低。x86指的是特定微處理器執行的一些計算機語言指令集，定義了芯片的基本使用規則。 

報告中，Greg Morrisett教授闡述了對 x86架構處理器指令集進行形式化建模和驗證的工作，建模和驗證利用定理證明輔助工具Coq進行，涵蓋了常用的100多條x86指令。Coq是一個定理證明輔助工具,用來開發數學證明,特別是表達程序及其形式規范,并驗證程序是否滿足規范。 

同時，他對基于派生(derivative)的正則表達式解析方法進行了介紹。他表示，通過使用派生離線地構造確定型有限自動機(DFA)表格，可以將現有的二進制x86機器碼解碼工具的效率提高100倍以上，并認為這種高效的、形式化的機器代碼分析方法可以廣泛應用于其他機器級別的程序分析和驗證任務中。 

Greg Morrisett教授的報告十分精彩，報告結束后，與會人員同Greg Morrisett教授對 Coq定理證明的細節以及正則表達式之外的文法的形式化解析等進行了深入廣泛交流。 

Greg Morrisett 是美國哈佛大學工程和應用科學學院的計算機科學系教授，他是程序語言和軟件系統驗證研究方向的專家。 

Greg Morrisett教授作報告

報告會現場