（不）可解的环路分析
摘要：自动生成不变量是计算机辅助分析概率性和确定性程序以及编译器优化的关键问题。虽然该问题一般是不可判定的，但对于受限循环类别的目标已经确立。由Kapur和Rodr''iguez-Carbonell在2004年引入的可解循环类别，可以通过模拟循环行为的递归方程的闭式解来自动计算不变量。本文建立了一种对于不可解循环的不变量综合技术。我们的方法自动划分程序变量，并识别所谓的“有缺陷”变量，以表征不可解性。我们考虑以下两个应用场景。首先，我们提出了一种新颖的技术，从有缺陷的单项式中自动生成具有闭式解的多项式，从而产生多项式循环不变量。第二，在给定一个不可解循环的情况下，我们综合出具有以下特性的可解循环：可解循环的不变量多项式与给定的不可解循环的不变量多项式完全相同。我们的实现和实验展示了我们的方法在确定性和概率性程序中的可行性和适用性。
作者：Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kov''acs, Marcel Moosbrugger, Miroslav Stankoviv{c}
论文ID：2306.01597
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-05