Seminar by Mr. Sumit Gulwani
Random Interpretation (Random testing + Abstract interpretation
Sumit Gulwani
Graduate Student
Dept of Computer Science
University of California Berekeley
USA
Date: Tue, Jan 4, 2005
Time: 3:45 PM
Venue: CS-101
Abstract
A sound and complete program analysis is undecidable. One commonly used approach is "random testing", which is complete (i.e., all bugs found are real bugs) but unsound (i.e., cannot prove absence of bugs). At the other extreme, we have the general class of sound program analyses called "abstract interpretation", wherein we pay a price for the hardness of program analysis in terms of having an incomplete analysis (i.e., it may report spurious errors or false positives), and by having algorithms that are complicated and have long running time. Taking inspiration from both these approaches, we have developed the idea of "random interpretation", which is more powerful than either of the approaches. Random interpretation is more complete, more efficient, and even simpler than the corresponding deterministic static analyses at the price of degrading soundness from absolute certainty to guarantee with arbitrarily high probability. The key idea in random interpretation is to execute the code fragment on a few random inputs in a non-standard 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 join 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.
In this talk, I will describe the random interpretation scheme for discovering/verifying properties of programs that use linear arithmetic operators, and programs that have been abstracted using uninterpreted functions. I will also describe how to discover these properties in an interprocedural setting.