一种寻找数值不变量的反例引导方法
软件工程
2019-03-29 v1
摘要
数值不变量（例如程序中数值变量之间的关系）代表了一类用于分析程序的有用属性。一般多项式不变量表示更复杂的数值关系，但它们在许多科学与工程应用中往往是必需的。我们提出了NumInv，这是一个实现了反例引导不变量生成（CEGIR）技术的工具，用于自动发现数值不变量，即数值变量之间的多项式等式与不等式关系。该CEGIR技术从程序执行迹中推断候选不变量，然后使用KLEE测试输入生成工具对照程序源代码对其进行检验。如果不变量不正确，KLEE会返回反例迹，从而帮助动态推断获得更好的结果。现有的CEGIR方法通常需要可靠的不变量，然而NumInv牺牲了可靠性，生成KLEE在特定时间范围内无法反驳的结果。这种设计以及将KLEE用作验证器，使得NumInv能够为许多具有挑战性的程序发现有价值和重要的数值不变量。初步结果表明，NumInv能生成所需的不变量，用于理解和验证涉及复杂算术运算的程序的正确性。我们还表明，NumInv能发现多项式不变量，这些不变量精确刻画了用于基准测试现有静态复杂度分析技术的程序的复杂度界限。最后，我们表明，与SOTA数值不变量分析工具相比，NumInv表现出竞争力。
引用
@article{arxiv.1903.12113,
title = {A Counterexample-guided Approach to Finding Numerical Invariants},
author = {ThanhVu Nguyen and Timos Antopoulos and Andrew Ruef and Michael Hicks},
journal= {arXiv preprint arXiv:1903.12113},
year = {2019}
}