使用内在定义的可预测验证
Predictable Verification using Intrinsic Definitions
AI总结：
本文提出用内在定义和单子映射替代递归来定义数据结构，并基于 Boogie 实现可预测验证，证明了一组数据结构操作程序的正确性。
摘要：
我们提出了一种使用内在定义来定义数据结构的新机制，该机制避免递归，转而利用满足局部条件的单子映射。我们表明，内在定义是一种强大的机制，能够自然地刻画多种数据结构。我们还表明，它们支持一种可预测的验证方法，使工程师能够编写幽灵代码来更新单子映射，并通过归约到可判定逻辑来执行验证。我们使用 Boogie 评估了我们的方法，并证明了一组操作数据结构的程序的正确性。
英文摘要：
We propose a novel mechanism of defining data structures using intrinsic definitions that avoids recursion and instead utilizes monadic maps satisfying local conditions. We show that intrinsic definitions are a powerful mechanism that can capture a variety of data structures naturally. We show that they also enable a predictable verification methodology that allows engineers to write ghost code to update monadic maps and perform verification using reduction to decidable logics. We evaluate our methodology using Boogie and prove a suite of data structure manipulating programs correct.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
