arXiv 1407.61242014-07-23cs.PL

命令式程序中数据结构性质的自动证明

Automating Proofs of Data-Structure Properties in Imperative Programs

Duc-Hiep Chu, Joxan Jaffar, Minh-Thai Trinh

摘要：

我们考虑动态操作数据结构的自动推理问题。最先进的方法仅限于展开和匹配（U+M）范式，其中谓词在被视为未解释之前通过从其定义中导出的（解）折叠操作进行转换。然而，验证具有迭代循环和多个函数调用的程序的证明义务通常不会屈服于这种范式。我们的贡献是一个证明方法-超越U+M -执行自动公式重写处理以前遇到的义务，在每个证明路径作为可能的归纳假设。这使我们第一次能够系统地推理出实际方案核查所产生的各种义务。我们展示了我们的证明规则的力量，常用的引理，从而关闭现有的国家的最先进的系统中剩余的差距。另一个影响，可能更重要的是，我们的方法重新获得了组合推理的能力，并表明使用用户提供的引理不再需要现有的基准集。这不仅消除了提出适当引理的负担，而且还显著地提高了验证过程，因为引理应用与展开相结合，通常会导致非常大的搜索空间。

英文摘要：

We consider the problem of automated reasoning about dynamically manipulated data structures. The state-of-the-art methods are limited to the unfold-and-match (U+M) paradigm, where predicates are transformed via (un)folding operations induced from their definitions before being treated as uninterpreted. However, proof obligations from verifying programs with iterative loops and multiple function calls often do not succumb to this paradigm. Our contribution is a proof method which -- beyond U+M -- performs automatic formula re-writing by treating previously encountered obligations in each proof path as possible induction hypotheses. This enables us, for the first time, to systematically reason about a wide range of obligations, arising from practical program verification. We demonstrate the power of our proof rules on commonly used lemmas, thereby close the remaining gaps in existing state-of-the-art systems. Another impact, probably more important, is that our method regains the power of compositional reasoning, and shows that the usage of user-provided lemmas is no longer needed for the existing set of benchmarks. This not only removes the burden of coming up with the appropriate lemmas, but also significantly boosts up the verification process, since lemma applications, coupled with unfolding, often induce very large search space.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

摘要：

英文摘要：

相关论文