Prism: Configurable Program Analysis
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:
Finding Optimum Abstractions in Parametric Dataﬂow Analysis.
X. Zhang, M. Naik, and H. Yang.
PLDI'13: ACM Conference on Programming Language Design and Implementation.
Abstractions from Tests.
M. Naik, H. Yang, G. Castelnuovo, and M. Sagiv.
POPL'12: ACM Symposium on Principles of Programming Languages.
[long version] [slides]
Scaling Abstraction Refinement via Pruning.
P. Liang and M. Naik.
PLDI'11: ACM Conference on Programming Language Design and Implementation.
Learning Minimal Abstractions.
P. Liang, O. Tripp, and M. Naik.
POPL'11: ACM Symposium on Principles of Programming Languages.
A Dynamic Evaluation of the Precision of Static Heap Abstractions.
P. Liang, O. Tripp, M. Naik, and M. Sagiv.
OOPSLA'10: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications.
This research is funded in part by NSF CAREER Award Adaptive Large-Scale Program Analysis.