从仿射到多项式：通过代数几何合成带分支的循环
编程语言
2025-09-30 v1 符号计算
代数几何
摘要
确保软件正确性仍是形式化程序验证中的根本挑战。一种有前景的做法依赖于寻找循环的多项式不变量。循环的多项式不变量是指在每次迭代前后都成立的程序属性。生成此类不变量是循环分析中的关键任务，但在一般情况下是不可判定的。最近出现的另一种方法聚焦于从不变量合成循环。然而，现有方法仅能从多项式不变量合成无守卫条件的仿射循环。本文解决更一般的问题，允许循环具有给定结构的多项式更新映射、守卫条件中的不等式以及任意形式的多项式不变量。我们使用代数几何工具设计并实现一种算法，计算出一组有限的多项式方程组，其解对应于满足给定不变量的所有非确定性分支循环。此外，我们引入了一类新的不变量，并为该类不变量提出了显著更高效的算法。换句话说，我们将合成循环的问题化简为求解具有有理系数的多元多项式系统的解。该最终步骤在我们的软件中通过SMT求解器实现。
引用
@article{arxiv.2509.25114,
title = {From Affine to Polynomial: Synthesizing Loops with Branches via Algebraic Geometry},
author = {Erdenebayar Bayarmagnai and Fatemeh Mohammadi and Rémi Prébet},
journal= {arXiv preprint arXiv:2509.25114},
year = {2025}
}