一句话：将可判定无解释程序扩展到别名感知映射更新，并在森林与单遍条件下判定堆程序内存安全。
本文研究堆操作程序自动验证的可判定性，重点是证明内存安全：程序分配、释放内存位置并操作堆指针时，不会解引用未分配位置。作者将近期关于可判定无解释程序子类的工作扩展到可更新映射的别名感知程序，并据此为内存安全设计判定算法。主要结果为：当初始已分配堆构成森林数据结构，且程序满足 streaming-coherent（直观上限制程序对数据结构只做单遍遍历）时，该内存安全问题可判定。作者在操作森林数据结构的库例程上进行实验，表明常见单遍算法常落入该可判定类，且判定过程能高效地验证它们。
We investigate the decidability of automatic program verification for programs that manipulate heaps, and in particular, decision procedures for proving memory safety for them. We extend recent work that identified a decidable subclass of uninterpreted programs to a class of alias-aware programs that can update maps. We apply this theory to develop verification algorithms for memory safety— determining if a heap-manipulating program that allocates and frees memory locations and manipulates heap pointers does not dereference an unallocated memory location. We show that this problem is decidable when the initial allocated heap forms a forest data-structure and when programs are streaming-coherent , which intuitively restricts programs to make a single pass over a data-structure. Our experimental evaluation on a set of library routines that manipulate forest data-structures shows that common single-pass algorithms on data-structures often fall in the decidable class, and that our decision procedure is efficient in verifying them.
@article{paperbot537,
title = {Deciding memory safety for single-pass heap-manipulating programs},
author = {Umang Mathur and Adithya Murali and Paul Krogmeier and P. Madhusudan and Mahesh Viswanathan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371103}
}