解决无法求解循环的不变量生成
摘要：自动生成不变量对于概率和确定性程序的计算机辅助分析和编译优化至关重要，这是一个具有挑战性的未解决问题。虽然这个问题通常是不可决定的，但对于受限循环的类别，这个目标已经得到解决。对于可解循环的类别，由Kapur和Rodr''iguez-Carbonell在2004年引入，可以根据模型循环行为的封闭解决方案自动计算不变量。本文建立了一个针对不可解循环（称为不可解循环）的不变量合成技术。我们的方法自动分割程序变量，并识别所谓的缺陷变量，以表征不可解性。我们还提出了一种新颖的技术，可以自动合成多项式，其中含有缺陷变量的多项式具有封闭解决方案，从而得到多项式循环不变量。我们的实现和实验证明了我们的方法对确定性和概率程序的可行性和适用性。
作者：Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kov''acs, Marcel Moosbrugger, Miroslav Stankoviv{c}
论文ID：2206.06943
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-06-15