使用平方和优化的基于属性多项式不变量生成
计算机科学中的逻辑
2015-03-25 v1
摘要
尽管抽象解释在理论上不限于特定类型的属性，但在实践中它主要被发展为计算可达集的线性过近似，即可程序的收集语义。用户给定属性的验证不易与通常使用数值抽象域的前向不动点计算兼容。我们在此提议依靠平方和规划来刻画一个属性驱动的多项式不变量。该不变量生成可由有界性，或者相反，由要避免的给定状态空间区域引导。虽然目标属性相对于程序语义未必是归纳的，我们的方法利用数值优化识别出一个更强的归纳多项式不变量。我们的方法适用于广泛的一类程序：由多项式更新的析取（if-then-else）组成的主 while 循环，例如分段多项式控制器。它已在各种程序上进行了评估。
引用
@article{arxiv.1503.07025,
title = {Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization},
author = {Assalé Adjé and Pierre-Loïc Garoche and Victor Magron},
journal= {arXiv preprint arXiv:1503.07025},
year = {2015}
}
备注
arXiv admin note: substantial text overlap with arXiv:1409.3941