EXPLORER : query- and demand-driven exploration of interprocedural control flow properties
Abstract
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Oct 23, 2015
- Source ID
- 10.1145/2858965.2814284
Entities
People
- Calvin Lin
- Işıl Dillig
- Xinyu Wang
- Yu Feng
Organizations
- Defense Advanced Research Projects Agency
- National Science Foundation
- University of Texas at Austin