结合策略迭代与半正定松弛以在静态分析中计算精确数值不变式
计算机科学中的逻辑
2019-03-14 v2 最优化与控制
摘要
我们引入了一个新域，用于通过抽象解释寻找程序的精确数值不变式。该域由非线性函数的水平集构成，推广了由 Manna、Sankaranarayanan 和 Sipma 提出的线性“模板”域。在二次模板的情况下，我们使用 Shor 的半正定松弛来导出语义泛函的可计算且精确的抽象，并表明抽象不动点方程可以通过结合策略迭代和半正定规划来精确求解。我们在一系列示例（滤波器、积分方案）上演示了该方法的优越性，包括一个退化示例（辛方案）。
引用
@article{arxiv.1111.5223,
title = {Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis},
author = {Assalé Adjé and Stéphane Gaubert and Eric Goubault},
journal= {arXiv preprint arXiv:1111.5223},
year = {2019}
}
备注
32 pages, 9 figures, preliminary version appeared in ESOP (European Symposium On Programming) 2010; LMCS 8 (1:1) 2012