Random Interpretation

Dr. Gulwani is a faculty candidate in CSE.
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, 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. In the first part of the talk, I will described few random interpretation based program analyses that are more efficient as well as simpler than their deterministic counterparts.

There are several interesting algorithmic challenges involved in improving the precision of program analyses (whether randomized or deterministic), such as extending an analysis to an interprocedural setting, combining two program analyses, and using Boolean reasoning to increase the precision of an analysis. In the second part of the talk, I will briefly describe automatic and efficient techniques that address these issues for certain classes of program analyses.