Randomized Resource-Aware Path-Sensitive static analysis

Abstract

Many interesting properties of programs can only be proved by a path-sensitive analysis. However, path sensitivity may drastically increase analysis time and memory consumption. For existing approaches, the amount of required resources is hard to predict in advance. As a consequence, in a particular analysis run available resources may either be wasted or turn out to be insufficient. In this paper, we propose a resource-aware approach to path-sensitive analysis that allows to control the maximal amount of required memory. It employs randomly-drawn hash functions to decide which paths to distinguish. Due to randomization, two analysis runs of the same program may yield different results. We show how to use this feature to trade analysis time for space.