CompCert编译优化步骤Tunnel.docx

西安交通大学本科毕业设计（论文）

摘要

PAGEII

PAGEI

摘要

随着软件行业的不断发展，计算机软件技术已经深入到社会生活的每个角落。在安全攸关软件行业，软件系统的可靠性一直是研究人员最关心的问题。编译器的正确性是保证软件系统可靠性的基础。编译器本身是庞大而又复杂的软件系统，现实中保证编译器的正确性并不容易。形式化验证技术能为编译器的正确性提供已知最强的保证，本题目目的是验证可信编译器CompCert的编译优化步骤Tunneling在并发程序分离编译场景下的正确性。

Tunneling是一个常见的编译优化步骤，CompCert已经验证了Tunneling编译优化步骤在串行