Farkas引理下的仿射不交不变量生成
摘要：生成循环不变量是一种经典问题，旨在自动化地生成对程序中可达状态集合进行过大估计的断言。我们考虑在仿射while循环（即带有仿射循环保护、条件分支和赋值语句的循环）中生成仿射不变量的问题，并探索自动化生成析取仿射不变量的方法。析取不变量是捕捉程序中析取特征（例如多个阶段、不同模式之间的转换等）的重要不变量类别，并且通常比带有这些特征的程序的合取不变量更精确。为了生成紧凑的仿射不变量，现有的约束求解方法已经研究了将法尔卡斯引理应用于合取仿射不变量的生成，但没有人考虑过析取仿射不变量的情况。
作者：Hongming Liu, Jingyu Ke, Hongfei Fu, Liqian Chen, Guoqiang Li
论文ID：2307.13318
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-03