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教授作报告

　　报告会现场