一群兴趣各异的模拟市民家庭

《Proceedings of the ACM on Programming Languages》：A Family of Sims with Diverging Interests

程序精化中提出μdiv-simulation弥合弱敏感发散模拟与规范模拟的空白，定义参数化模拟概念覆盖12种模拟并建立多种“直到”推理技术，在Rocq中实现并通过选择树和Verified Compilation案例验证。

　　

摘要人工智能摘要

要查看此由人工智能生成的摘要，您必须拥有高级访问权限。

了解更多登录

摘要

摘要

模拟是程序精炼中广泛使用的概念。本文讨论并比较了几种模拟方法，特别是那些既弱又对发散敏感的模拟方法。在证明辅助工具中执行的复杂模拟证明（例如在经过验证的编译环境中）通常依赖于规范模拟的变体，而这些变体对于对发散敏感的弱模拟来说并不完备。我们提出使用μdiv-simulation来填补这一空白，这是一种新型的模拟概念，它与传统的对发散敏感的弱模拟等价，并且设计得与现代的规范模拟表征一样易于使用。然后，我们定义了一个参数化的模拟概念，涵盖了强模拟、弱模拟、μdiv-simulation以及另外9种模拟概念，并为这12种概念共同建立了各种“直到”推理技术。我们的结果在Rocq框架中得到了形式化，并在两个案例研究中得到了验证：选择树（Choice Trees）和CompCertpass。经过验证的编译是我们研究的主要动机，但由于我们使用的是抽象的LTS（Long-Term Safety）框架，我们的结果也与其他使用对发散敏感的弱模拟的领域（如模型检测）相关。

人工智能摘要

人工智能生成的摘要（实验性)

该摘要是使用自动化工具生成的，并非由文章作者编写或审阅的。它旨在帮助发现、帮助读者评估相关性，并协助来自相关研究领域的读者理解本文的工作。它旨在补充作者提供的摘要，后者仍然是文章的官方摘要。完整文章才是权威版本。点击此处了解更多。

点击此处对摘要的准确性、清晰度和实用性进行评论。您的反馈将有助于改进未来的版本。

要查看此由人工智能生成的通俗语言摘要，您必须拥有高级访问权限。