递归存在下通过堆的交互

几乎所有现代命令式编程语言都包含动态操作堆的操作，例如分配和释放对象以及更新引用字段。在递归过程和局部变量存在的情况下，程序与堆的交互会变得相当复杂，因为无限数量的对象既可以通过局部变量在调用栈上分配，也可以通过引用字段匿名地在堆上分配。因此，静态分析通常是不可判定的。本文研究了一种用于堆操作的简单命令式语言中，具有无界对象分配的递归程序的验证问题。我们为该语言提出了一种改进的语义，使用了一种精确的抽象。对于任何具有有界可见堆的程序，即在执行的任何时刻从变量可达的对象数量是有界的，这种抽象是其行为的有限表示，即使状态中可能出现无限数量的对象。因此，对于此类程序，模型检测是可判定的。最后，我们引入了一种用于描述堆的时序属性的规约语言，并讨论了针对堆操作程序对这些属性进行模型检测的问题。