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:
This research is funded in part by NSF CAREER Award Adaptive Large-Scale Program Analysis.