一句话：提出用满足局部条件的 monadic maps 定义数据结构，实现可预测的验证。
论文针对递归数据结构定义导致验证难以预测的问题，提出“内在定义”（intrinsic definitions）：不使用递归，而是用满足局部条件的 monadic maps 来定义数据结构。作者表明该机制能自然刻画多种数据结构，并支持可预测的验证方法：工程师编写 ghost code 更新 monadic maps，再将验证任务归约到可判定逻辑。基于 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 B oogie and prove a suite of data structure manipulating programs correct.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{MuraliRM24,
title = {Predictable Verification using Intrinsic Definitions},
author = {Adithya Murali and Cody Rivera and P. Madhusudan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656450}
}