Random Interpretation
(Random Testing + Abstract Interpretation)
Randomized Algorithms for Formal Verification

Program Analysis

Theorem Proving

Model Checking

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 intepretation.

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 and for the theory of uninterpreted functions. 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 (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? Here are some directions worth considering.

### Papers

• Program Analysis using Random Interpretation [abstract |ps |pdf |bibtex], Sumit Gulwani, Phd Dissertation, UC-Berkeley, 2005.

• Precise Interprocedural Analysis using Random Interpretation [abstract |ps |pdf |ppt |bibtex], Sumit Gulwani and George Necula, To appear in the 32nd Annual ACM Symposium on Principles of Programming Languages (POPL 2005)

• Global Value Numbering using Random Interpretation, [ abstract |ps |pdf |ppt |bibtex], Sumit Gulwani, George Necula, In the 31st Annual ACM Symposium on Principles of Programming Languages (POPL 2004)
• Full version appears as UCB technical report CSD-03-1296 [ps]

• Discovering Affine Equalities using Random Interpretation [ abstract |ps |pdf |ppt |bibtex], Sumit Gulwani and George Necula, In the 30th Annual ACM Symposium on Principles of Programming Languages (POPL 2003)

• Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions [abstract |ps |pdf |ppt |bibtex], Sumit Gulwani and George Necula, In the 11th Static Analysis Symposium (SAS 2004)
• Full version appears as UCB technical report CSD-04-1325 [ps]

• A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols [ abstract |ps |pdf |ppt |bibtex], Sumit Gulwani and George Necula, In the 19th Conference on Automated Deduction (CADE 2003)
• Full version appears as UCB technical report CSD-03-1241 [ps]