Program Analysis using Random Interpretation

Abstract

Random interpretation is a new program analysis technique that uses the power of randomization to verify and discover program properties. It is inspired by, and combines the strengths of, the two complementary techniques for program analysis: random testing and abstract interpretation. Random testing is simple and finds real bugs in programs, but cannot prove absence of bugs. Abstract interpretation, on the other hand, is a class of sound and deterministic program analyses that find all bugs, but also report spurious bugs (false positives). Often these analyses are complicated and have long running time. This thesis describes few random interpretation based program analyses that are more efficient as well as simpler than their deterministic counterparts that had been state-of-the-art for almost 30 years. This thesis also describes how to extend some of these intraprocedural analyses to an interprocedural setting. We also discuss our experience experimenting with these algorithms.