基于性质的多项式不变式的平方和优化生成
Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization
摘要：
虽然抽象解释在理论上并不局限于特定类型的属性，但在实践中，它主要用于计算可达集的线性过近似。程序的收集语义。用户提供的属性的验证不容易与通常的前向不动点计算使用数值抽象域兼容。我们建议在这里依靠平方和编程来表征属性驱动的多项式不变。这种不变量的生成可以由有界性来指导，或者相反，可以由要避免的状态空间的给定区域来指导。虽然目标属性不一定是归纳相对于程序语义，我们的方法确定了一个更强的归纳多项式不变量使用数值优化。我们的方法适用于广泛的程序集：一个主要的，而循环组成的析取（如果，然后，否则）的多项式更新，例如分段多项式控制器。它已在各种方案中得到评估。
英文摘要：
While abstract interpretation is not theoretically restricted to specific kinds of properties, it is, in practice, mainly developed to compute linear over-approximations of reachable sets, aka. the collecting semantics of the program. The verification of user-provided properties is not easily compatible with the usual forward fixpoint computation using numerical abstract domains. We propose here to rely on sums-of-squares programming to characterize a property-driven polynomial invariant. This invariant generation can be guided by either boundedness, or in contrary, a given zone of the state space to avoid. While the target property is not necessarily inductive with respect to the program semantics, our method identifies a stronger inductive polynomial invariant using numerical optimization. Our method applies to a wide set of programs: a main while loop composed of a disjunction (if-then-else) of polynomial updates e.g. piecewise polynomial controllers. It has been evaluated on various programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
