C语言子集Clight的机械化语义
编程语言
2009-09-18 v1
摘要
本文介绍了C语言的一个大型子集Clight的形式语义。Clight包括指针算术、"struct"和"union"类型、C循环以及结构化的"switch"语句。Clight是CompCert验证编译器的源语言。Clight的形式语义是一种大步操作语义，它观察终止和发散的执行，并生成输入/输出事件轨迹。Clight的形式语义使用Coq证明助手进行了机械化。除了Clight的语义，本文还描述了它在CompCert验证编译器中的集成以及验证该语义的几种方法。
引用
@article{arxiv.0901.3619,
title = {Mechanized semantics for the Clight subset of the C language},
author = {Sandrine Blazy and Xavier Leroy},
journal= {arXiv preprint arXiv:0901.3619},
year = {2009}
}
备注
Journal of Automated Reasoning (2009)