.png){kind=icon}
返回
Denotation-based Compositional Compiler Verification
.png){kind=icon}
PRE
AI
DOI：10.1145/3797874.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
编译器验证中期望但具有挑战性的属性是组合性，即程序的编译正确性可以从其子结构（从语句、函数到模块）的正确性中逐步推导出来。本文提出了一种基于指称语义的新型编译器验证框架，以实现更好的组合性，相比基于小步操作语义和模拟理论的先前方法。我们的指称语义由语义函数定义，这些函数将语法组件映射到一个由多个行为集组成的语义域，编译器正确性通过源程序和目标程序语义域之间的行为精化建立。本文的主要贡献包括为开放模块提出指称语义、一种新颖的语义链接算子和一种统一各种行为精化的精化代数，使编译器验证具有结构化和组合性。此外，我们的形式化方法捕捉了程序的全部含义，弥合了传统幂域基指称语义与编译器验证的实际需求之间的差距。我们将基于指称的框架应用于验证Compcert的前端和简单命令式语言原型上的典型优化。结果表明，从子语句到语句、从函数到模块以及从模块到整个程序的组合性可以有效地实现。
Keyword:
compiler verification
denotational semantics
compositionality
CompCert
期刊
A
IF:
1.6
论文数:
10
被引数:
0
机构
引用论文
暂无论文信息