在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程

• 作者: 李凌 李璜华 王生原
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 语法分析 LR(1)分析器 形式化验证 Lustre?语言 CompCert Coq
• 年，卷（期）: 2020,（6）
• 所属期刊栏目: 智能软件工程
• 页码范围: 8-15
• 页数: 8页
• 分类号: TP314
• 字数: 12406字
• 语种: 中文
• DOI: 10.11896/jsjkx.191000173

摘要

Jourdan等在其2012年发表的论文"Validating LR(1)Parsers"中提出了一种形式化验证语法分析器的方法,并将其成功地应用于CompCert编译器(2.3以上版本)的语法分析器验证中.借助这种方法,文中完成了L2C项目中的Lustre?语言语法分析器的形式化验证,实现了开源L2 C编译器前端语法分析器的两个选项之一.首先对这一语法分析器的实现进行了论述,其中包括有参考价值的技术细节;随后分析了该语法分析器的运行性能及正确性;最后对如何将这一方法推广至更一般的应用场景进行了总结.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王生原	清华大学计算机科学与技术系	33	235	8.0	14.0
2	李凌	清华大学计算机科学与技术系	11	15	2.0	3.0
3	李璜华	清华大学计算机科学与技术系	1	0	0.0	0.0