Embracing a mechanized formalization gap
Embracing a mechanized formalization gap
复制标题
拥抱机械化正规化差距
DOI：
10.1145/3314221.3322484
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Stephanie Weirich
中科院分区：
文献类型：
--
作者：
Antal Spector;Joachim Breitner;Yao Li;Stephanie Weirich
如果一个代码库是如此庞大和复杂，以至于完全的机械验证是难以处理的，我们还能应用并受益于验证方法吗？我们表明，通过允许有意的机械化形式化差距，我们可以缩小和简化模型，直到它是可管理的，同时仍然保留一个有意义的、声明性的文档连接到原始的、未修改的源代码。具体来说，我们使用hs-to-coq将Haskell编译器GHC的核心部分翻译成Coq，并验证与术语变量使用相关的不变量。
If a code base is so big and complicated that complete mechanical verification is intractable, can we still apply and benefit from verification methods? We show that by allowing a deliberate mechanized formalization gap we can shrink and simplify the model until it is manageable, while still retaining a meaningful, declaratively documented connection to the original, unmodified source code. Concretely, we translate core parts of the Haskell compiler GHC into Coq, using hs-to-coq, and verify invariants related to the use of term variables.
影响因子：
1.1
作者：
Filipovic I
通讯作者：
Filipovic I