paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Polynomial Invariants for Affine Programs

仿射程序的多项式不变量
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 3/10 · 该论文属于程序分析与程序验证中的代数不变量生成，理论上与静态分析相关；但未涉及用户当前重点关注的 LLM/Agent、浮点程序分析或贝叶斯程序分析等交叉方向，也缺少与 AI 工具或工业落地的结合。引用 1 inbox
Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, James Worrell
程序分析与抽象解释程序验证
crossref: 2026-09-12

AI 速览

一句话：提出计算仿射程序各位置最强多项式（代数）不变量的算法，核心是计算有理矩阵生成半群的 Zariski 闭包。

论文研究仿射程序的最强多项式不变量生成问题。仿射程序只含非确定性分支，所有赋值均为仿射表达式。作者提出一种算法，可对程序每个控制位置计算在该位置成立的最强多项式（代数）不变量，即刻画所有成立的多项式等式。其核心工具是一个独立的代数结果：给定同维有理方阵的有限集合，能够计算它们所生成半群的 Zariski 闭包。由于循环中变量变换可表示为矩阵乘法，不变量集合对应于该半群作用下的代数不变量，因此 Zariski 闭包的计算直接给出最强不变量的精确刻画。该工作将代数几何方法引入程序分析，为仿射程序不变量提供可计算性结果。

问题
如何精确计算仿射程序每个控制位置成立的最强多项式（代数）不变量。
方法
把仿射赋值与循环建模为有理矩阵生成的半群，利用可计算其 Zariski 闭包的代数结果来刻画所有多项式不变量。
评估
摘要未报告实验评估；文章以算法和独立代数定理（Zariski 闭包可计算）作为主要结果。
原文摘要（Abstract）

We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching and all of whose assignments are given by affine expressions). Our main tool is an algebraic result of independent interest: given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot4316,
  title = {Polynomial Invariants for Affine Programs},
  author = {Ehud Hrushovski and Joël Ouaknine and Amaury Pouly and James Worrell},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209142}
}