This paper describes a general framework and its implementation in a tool called EXPLORER for statically answering a class of interprocedural control flow queries about Java programs. EXPLORER allows users to formulate queries about feasible callstack configurations using regular expressions, and it employs a precise, demand-driven algorithm for answering such queries. Specifically, EXPLORER constructs an automaton A that is iteratively refined until either the language accepted by A is empty (meaning that the query has been refuted) or until no further refinement is possible based on a precise, context-sensitive abstraction of the program. We evaluate EXPLORER by applying it to three different program analysis tasks, namely, (1) analysis of the observer design pattern in Java, (2) identification of a class of performance bugs, and (3) analysis of inter-component communication in Android applications. Our evaluation shows that EXPLORER is both efficient and precise.
CITATION STYLE
Feng, Y., Wang, X., Dillig, I., & Lin, C. (2015). EXPLORER : query- And demand-driven exploration of interprocedural control flow properties. ACM SIGPLAN Notices, 50(10), 520–534. https://doi.org/10.1145/2814270.2814284
Mendeley helps you to discover research relevant for your work.