Prism: Adaptive Large-Scale Program Analysis

What's New
About

A central challenge in static analysis concerns how to efficiently find a suitable program abstraction for proving a program query.  The PRISM project is exploring this problem in the setting of parametric static analyses.

In this setting, a static analysis takes a program query q and an abstraction from a family A, and attempts to prove the query using the abstraction. Different abstractions in the family have different precision/cost tradeoff for a given query. 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 query?
    • Necessary conditions [POPL'12]: What is a necessary condition on abstractions in a given family for proving a given query?
    • Impossibility [PLDI'13]: What queries 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 a query. Moreover, different queries in the same program require different abstractions. We are exploring techniques for efficiently searching suitable abstractions. Examples include machine learning [POPL'11], dynamic analysis [POPL'12], and meta analysis [PLDI'11, PLDI'13].

Our current focus is on reasoning about the heap and concurrency.  Such reasoning is central to virtually any analysis of imperative programs.

Papers
People
Alumni