扰动仿射算术在数值程序分析中的不变量计算
Perturbed affine arithmetic for invariant computation in numerical program analysis
AI总结:
提出一种新的抽象解释域,通过序与拓扑的相互作用,证明不动点迭代收敛于稳定线性递归滤波器(任意阶)的有限精确不变量,并适用于某些非线性方案。
摘要:
我们完整描述了一个用于数值程序抽象解释的新域。在该域中,不动点迭代被证明对于(至少)任意阶稳定线性递归滤波器类收敛到有限精确不变量。良好证据表明,它对于某些非线性方案也表现良好。该结果以及域的结构依赖于序与拓扑之间的有趣相互作用。
英文摘要:
We completely describe a new domain for abstract interpretation of numerical programs. Fixpoint iteration in this domain is proved to converge to finite precise invariants for (at least) the class of stable linear recursive filters of any order. Good evidence shows it behaves well also for some non-linear schemes. The result, and the structure of the domain, rely on an interesting interplay between order and topology.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。