Bias-variance tradeoffs in program analysis
Bias-variance tradeoffs in program analysis
复制标题
DOI：
10.1145/2535838.2535853
复制
发表时间：
2014-01
期刊：
影响因子：
--
通讯作者：
Rahul Sharma;A. Nori;A. Aiken
中科院分区：
文献类型：
--
作者：
Rahul Sharma;A. Nori;A. Aiken
经常出现的情况是，提高程序分析的精度会导致更差的结果。我们的论文认为，这种现象是使用精确抽象域作为推断程序强不变量的基础的能力受到基本限制的结果。我们表明，偏差-方差权衡，一个来自学习理论的想法，可以用来解释为什么更精确的抽象不一定会带来更好的结果，并提供了应对此类限制的实用技术。学习理论使用一个被称为VC维的组合量来捕捉精度。我们计算了不同抽象的VC维，并报告了它作为程序分析的精度度量的有用性。我们在一个名为Yogi的工业强度计划验证工具上评估交叉验证，这是一种解决偏差-方差权衡的技术。与当前的生产版本相比，使用交叉验证生成的工具具有更好的运行时间、发现新的缺陷和更少的超时。最后，我们对如何处理程序分析中的偏差-方差权衡提出了一些建议。
It is often the case that increasing the precision of a program analysis leads to worse results. It is our thesis that this phenomenon is the result of fundamental limits on the ability to use precise abstract domains as the basis for inferring strong invariants of programs. We show that bias-variance tradeoffs, an idea from learning theory, can be used to explain why more precise abstractions do not necessarily lead to better results and also provides practical techniques for coping with such limitations. Learning theory captures precision using a combinatorial quantity called the VC dimension. We compute the VC dimension for different abstractions and report on its usefulness as a precision metric for program analyses. We evaluate cross validation, a technique for addressing bias-variance tradeoffs, on an industrial strength program verification tool called YOGI. The tool produced using cross validation has significantly better running time, finds new defects, and has fewer time-outs than the current production version. Finally, we make some recommendations for tackling bias-variance tradeoffs in program analysis.