Prism: Configurable Program Analysis

What's New

A central challenge in program analysis concerns how to efficiently find a suitable program abstraction for resolving a program assertion.  The PRISM project is exploring this problem in the setting of configurable program analyses.

In this setting, a program analysis takes a program assertion q and an abstraction from a family A, and attempts to resolve the assertion using the abstraction. Different abstractions in the family have different precision/cost tradeoff for a given assertion. We are exploring the following problems unique to this setting:

  • New Analysis Questions: Our setting poses several new analysis questions outlined below:

    • Minimal abstractions [POPL'11]: What is the coarsest abstraction in a given family that is capable of proving a given assertion?
    • Necessary conditions [POPL'12]: What is a necessary condition on abstractions in a given family for proving a given assertion?
    • Impossibility [PLDI'13]: What assertions are impossible to prove using a given family of abstractions?

  • New Search Algorithms: In practice, families of abstractions are exponential in program size or even infinite. Most abstractions in a family are too imprecise or too costly to prove an assertion. Moreover, proving different assertions in the same program requires different abstractions. We are exploring new algorithms to efficiently find suitable abstractions, including ones based on machine learning, testing, and constraint solving. 

This research is funded in part by NSF CAREER Award Adaptive Large-Scale Program Analysis.