问答
高级检索
C程序的编译验证是形式化验证领域的一个重要问题，已有工作依赖基于区块的内存模型，而该模型难以支持局部内存结构转换的模块化验证，也不能被轻易拓展以描述更复杂的内存性质，这些问题极大阻碍了C程序编译验证方法的进一步发展。为解决上述问题，我们提出了一种对传统内存模型进行抽象的方法，其关键技术是通过将内存区块抽象表述为名义名字，以移除内存状态中的全局约束。通过整合抽象内存模型和CompCert，我们实现了名为Nominal CompCert的通用C程序编译验证框架，并用模块化验证、端到端完整编译过程的正确性验证检验了该框架的有效性。
汪宇霆
问答