Discovering affine equalities using random interpretation

被引:11
作者
Gulwani, S [1 ]
Necula, GC [1 ]
机构
[1] Univ Calif Berkeley, Berkeley, CA 94720 USA
关键词
algorithms; theory; verification; affine relationships; linear equalities; random interpretation; randomized algorithm;
D O I
10.1145/640128.604138
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We present a new polynomial-time randomized algorithm for discovering affine equalities involving variables in a program. The key idea of the algorithm is to execute a code fragment on a few random inputs, but in such a way that all paths are covered on each run. This makes it possible to rule out invalid relationships even with very few runs. The algorithm is based on two main techniques. First, both branches of a conditional are executed on each run and at joint points we perform an affine combination of the joining states. Secondly, in the branches of an equality conditional we adjust the data values on the fly to reflect the truth value of the guarding boolean expression. This increases the number of affine equalities that the analysis discovers. The algorithm is simpler to implement than alternative deterministic versions, has better computational complexity, and has an extremely small probability of error for even a small number of runs. This algorithm is an example of how randomization can provide a trade-off between the cost and complexity of program analysis, and a small probability of unsoundness.
引用
收藏
页码:74 / 84
页数:11
相关论文
共 12 条
[11]  
Pnueli A, 1998, LECT NOTES COMPUT SC, V1384, P151, DOI 10.1007/BFb0054170
[12]  
ROSEN BK, 1988, POPL 88, P00012