EXPLORER : query- and demand-driven exploration of interprocedural control flow properties

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 cise, 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. Categories and ...

• Type: Journal
• Year: 2015
• Where: OOPSLA
• Authors: Yu Feng, Xinyu Wang, Isil Dillig, Calvin Lin
• Keywords: OOPSLA 2015, Security Privacy