Preserving Separation Logic Specifications through Compilation 待解读
新用户看这篇论文该怎么开始
- 先点「赞助解读」，AI 会把论文转成可直接执行的行动清单。
- 看完“可执行改进行动”后，可快速决定是否值得立项。
- 用上面的卡片内容直接发给团队，减少重复阅读。
摘要
Program specifications in separation logic describe ownership of resources and serve as logical interfaces for local reasoning. Compiler correctness, expressed as semantics preservation, does not by itself supply such an interface for compiled code, because it does not explicitly relate source and target resources and assertions. We investigate WP-preserving compilation: when a compiler translates a source program, the weakest preconditions that the program satisfies in a separation logic carry over to the compiled program. Our proof technique consists of a resource-aware simulation over interaction trees: it relates the resources required by corresponding source and target events, and tracks ownership through target operations, such as register accesses, that have no source counterpart. We apply the approach to a compiler from a structured imperative language to an assembly-like language, first for closed programs and then extended with modules and function calls. In the extended setting, each module can be verified in the source logic and compiled separately; its specifications carry over to the compiled module and are preserved when compiled modules are linked. All results are mechanized in Rocq.
分析报告
暂无报告。点击“分析”开始生成。
个性化解读 与社区共享解读不同
用自己的话告诉 AI 你想要什么样的解读（比如"用大白话讲给非专业人士听"、"重点分析对我们团队 RAG 系统的可迁移性"），生成一份只属于你自己的版本；生成后也可以选择设为"愿意共享"，被更多人看到、点赞。