机械验证计算摘要解释
Mechanically Verified Calculational Abstract Interpretation
摘要：
计算抽象解释（Calculational Abstract Interpretation）是一种由Cousot长期倡导的技术，用于从程序设计语言的形式语义中导出正确的构造抽象解释器。本文讨论了使用证明助手导出正确的构造验证抽象解释器的问题。我们确定了几个技术挑战，以克服的目的是支持验证计算抽象的解释，是忠实于现有的纸和纸的证明，支持计算与伽罗瓦连接一般，并使验证静态分析从这些证明提取。为了迎接这些挑战，我们开发了一个理论的伽罗瓦连接在一元风格，包括规格的影响。精确的计算可能是经典的推理，而纯计算具有可提取的计算内容。在规范和实现的世界之间移动是由我们的元理论实现的。为了验证我们的方法，我们给出了Cousot的“通用抽象解释器的计算设计”的第一个机械验证的正确性证明。“我们的证明“通过微积分”紧密遵循原来的纸笔证明，并支持提取一个验证过的静态分析器。
英文摘要：
Calculational abstract interpretation, long advocated by Cousot, is a technique for deriving correct-by-construction abstract interpreters from the formal semantics of programming languages. This paper addresses the problem of deriving correct-by-verified-construction abstract interpreters with the use of a proof assistant. We identify several technical challenges to overcome with the aim of supporting verified calculational abstract interpretation that is faithful to existing pencil-and-paper proofs, supports calculation with Galois connections generally, and enables the extraction of verified static analyzers from these proofs. To meet these challenges, we develop a theory of Galois connections in monadic style that include a specification effect. Effectful calculations may reason classically, while pure calculations have extractable computational content. Moving between the worlds of specification and implementation is enabled by our metatheory. To validate our approach, we give the first mechanically verified proof of correctness for Cousot's "Calculational design of a generic abstract interpreter." Our proof "by calculus" closely follows the original paper-and-pencil proof and supports the extraction of a verified static analyzer.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
