报告题目：编译器形式化验证及L2C可信编译器简介

报告人：王生原，清华大学

报告简介：对于编译器的“误编译”问题，大家都司空见惯、习以为常了。然而，对于安全关键系统的验证而言，必须考虑因编译器引入的错误，否则花大力气在源程序级的验证工作可能在目标程序级失效。实际上，如航空领域的RTCA DO-178B/C标准，编译器属于需要鉴定的工具类软件，需要按照机载软件的要求一样对待。最严格的验证手段就是采用形式化方法，近年来，有关编译器形式化验证的研究工作取得了长足的进步，达到了实用化水平，为未来新的工业标准制定奠定了强有力的基础。本次报告将对编译器形式化验证的主要技术及研究进展进行概述，并对清华大学L2C可信编译器项目的开展情况进行简介。L2C项目致力于从高级建模语言（类Lustre的同步数据流语言）到C语言的可信翻译，并与著名的CompCert编译器衔接，形成从建模语言到汇编语言的可信编译工具。

报告人简介：生于1964年，分别于太原理工大学、西安电子科技大学、北京大学获得计算机专业学士（1984年）、硕士（1987年）、博士（2001年）学位，曾任教于兰州大学计算机系多年，自2001年8月起任清华大学计算机系副教授，主讲“编译原理”和“形式语言与自动机”两门本科生核心课程，主要从事程序设计语言、编译器、形式化方法等领域的研究，近几年主要致力于面向关键领域软件开发工具的研发工作，2010年创立并主持L2C可信编译器项目，相关工作在工业领域得到初步应用。