Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes
Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes
复制标题
迈向 C0 编译器的形式验证：代码生成和实现正确性
DOI：
10.1109/sefm.2005.51
复制
发表时间：
2005
影响因子：
2.8
通讯作者：
Elena Petrova
中科院分区：
文献类型：
--
作者：
Dirk Leinenbach;W. Paul;Elena Petrova
本着著名的CLI堆栈项目的精神，Verisoft项目旨在对整个计算机系统的广泛验证，包括硬件，系统软件，编译器和通信应用程序，并特别关注工业应用程序。 Verisoft项目中使用的主要编程语言是C0（与Misra C相似的C子集）。本文报告了（i）C0的操作小步骤语义，该语义是在Isabelle/Hol中正式化的，（ii）编译器从C0到DLX机器语言的正式规格，以Isabelle/Hol（III）（iii）纸和铅笔的形式该编译器的正确性证明以及此证明的正式验证工作的状态，以及（iv）在C0中实施编译器，以及Isabelle/HOL中实施中实施的正式证明，该证明产生与规范相同的代码。
In the spirit of the famous CLI stack project the Verisoft project aims at the pervasive verification of entire computer systems including hardware, system software, compiler, and communicating applications, with a special focus on industrial applications. The main programming language used in the Verisoft project is C0 (a subset of C which is similar to MISRA C). This paper reports on (i) an operational small steps semantics for C0 which is formalized in Isabelle/HOL, (ii) the formal specification of a compiler from C0 to the DLX machine language in Isabelle/HOL, (iii) a paper and pencil correctness proof for this compiler and the status of the formal verification effort for this proof, and (iv) the implementation of the compiler in C0 and a formal proof in Isabelle/HOL that the implementation produces the same code as the specification.