一种递归方程的序数理论框架用于静态成本分析——动态推断非线性不等式不变式

递归方程在静态成本分析中发挥着核心作用，人们可以将其视为程序的抽象，并用于推断在不使用具体数据的情况下获取的资源使用信息。这种信息通常表示为输入数据大小的函数。更一般地，递归方程越来越多地用于自动获取非线性数值不变式。然而，现有的递归求解器和成本分析器在处理源自成本分析的递归的（complex）特征时存在严重限制。我们通过发展一种新的序数理论框架来解决这一挑战，其中将递归视为算子，其解作为不动点，这允许利用强大的前/后不动点搜索技术。我们证明了有用性质，提供了原则和见解，以便开发技术并将其组合以设计新的求解器。我们还实现并实验评估了一个基于优化的该方法的实例。结果相当令人鼓舞：我们的原型工具超过了现有的成本分析器和递归求解器，能够在合理时间内推断出针对代表各种程序行为的复杂递归的紧密的非线性下/上界。