Powerpoint Slides on Random Interpretation
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.