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:
- On Abstraction Refinement for Program Analyses in Datalog.
Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, and Hongseok Yang.
PLDI'14: ACM Conference on Programming Language Design and Implementation.
Finding Optimum Abstractions in Parametric Dataﬂow Analysis.
Xin Zhang, Mayur Naik, and Hongseok Yang.
PLDI'13: ACM Conference on Programming Language Design and Implementation.
Abstractions from Tests.
Mayur Naik, Hongseok Yang, Ghila Castelnuovo, and Mooly Sagiv.
POPL'12: ACM Symposium on Principles of Programming Languages.
[long version] [slides]
Scaling Abstraction Refinement via Pruning.
Percy Liang and Mayur Naik.
PLDI'11: ACM Conference on Programming Language Design and Implementation.
Learning Minimal Abstractions.
Percy Liang, Omer Tripp, and Mayur Naik.
POPL'11: ACM Symposium on Principles of Programming Languages.
A Dynamic Evaluation of the Precision of Static Heap Abstractions.
Percy Liang, Omer Tripp, Mayur Naik, and Mooly 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.