Randomized Algorithms for Formal Verification

Powerpoint Slides on Random Interpretation (opens in new tab)

Introduction

A sound and complete program analysis is provably hard. We typically pay a price for the hardness of program analysis in terms of having an incomplete (i.e. conservative) analysis, or by having algorithms that are complicated and have long running-time. It is interesting to consider if we can pay for this hardness by compromising soundness a little bit (and thus benefit by having simpler and more efficient and complete algorithms). By compromising soundness, we mean that judgements may be unsound, but with very low probability. Furthermore, we can predict and control this error probability and make it so small that for practical purposes, it does not hurt at all. We can make the error probability smaller than the probability of a hardware error in a computer, or the probability of a meteorite striking one’s computer in the next microsecond. We have developed a set of randomized algorithms for program analysis, which are more efficient and precise than their deterministic counterparts. These algorithms are quite simple, however their probabilistic soundness proofs have been the challenging part. These algorithms seem to have a common theme, which we call random interpretation.

Random interpretation is similar to abstract interpretation, which is a well-known technique for program analysis. The key idea in random interpretation is to execute the code fragment on a few random inputs in a contrived manner, which includes giving random linear interpretations to the operators in the program. Both branches of a conditional are executed on each run and at joint points we perform a random affine combination of the joining states. 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.

We have described random interpretation schemes for the theory of linear arithmetic (opens in new tab) and for the theory of uninterpreted functions (opens in new tab). Both these random interpretation schemes have a better computational complexity and are simpler to implement than the corresponding abstract interpretation schemes. These random interpretation schemes are intraprocedural. Recently, we have described a generic technique to extend any intraprocedural random interpretation scheme to perform an interprocedural analysis (opens in new tab) (essentially by computing random summaries of the procedures). The next step is to come up with a random interpretation scheme for the combined theory of linear arithmetic and uninterpreted function symbols. More generally, we are working on a generic strategy to combine any two random interpretation schemes.

Can we benefit by applying similar ideas to other program analysis problems and decision procedures for other theories?