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:
Our current focus is on reasoning about the heap and concurrency. Such reasoning is central to virtually any analysis of imperative programs.