Reference
Abstract
We present jumping, a form of selective control-flow abstraction useful for improving the scalability of goal-directed static analyses. Jumping is useful for analyzing programs with complex control-flow such as event-driven systems. In such systems, accounting for orderings between certain events is important for precision, yet analyzing the product graph of all possible event orderings is intractable. Jumping solves this problem by allowing the analysis to selectively abstract away control-flow between events irrelevant to a goal query while preserving information about the ordering of relevant events. We present a framework for designing sound jumping analyses and create an instantiation of the framework for performing precise inter-event analysis of Android applications. Our experimental evaluation showed that using jumping to augment a precise goal-directed analysis with inter-event reasoning enabled our analysis to prove 90--97\% of dereferences safe across our benchmarks.
BibTeX
@string{OOPSLA = "ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA)"}
@inproceedings{controlfeasibility-oopsla15,
author = {Sam Blackshear and Bor-Yuh Evan Chang and Manu Sridharan},
title = {Selective Control-Flow Abstraction via Jumping},
booktitle = OOPSLA,
year = {2015},
pages = {163-182},
}