Scalable Parametric Static Analysis

Abstract

Parametric static analysis allows choosing a parameter value to balance the precision and cost of the instantiated analysis. We propose an efficient approach to either find a cheapest parameter value to prove a given query or show that no such parameter value exists. Our approach is based on refinement, as in CEGAR (counterexample-guided abstraction refinement), but applies a novel meta-analysis to abstract counterexample traces to efficiently find parameter values that are incapable of proving the query. We formalize our approach in a generic framework and apply it to two parametric analyses: a thread-escape analysis and a type-state analysis. The thread-escape analysis is implemented and applied to eight Java benchmarks comprising 2.5 MLOC. Our experiments show that our approach is effective in practice: for our four largest benchmarks, searching 2⁹K[superscript] parameter values for each of 10K queries on average per benchmark, it finds a cheapest one for proving 46% queries and shows that none exists for 37% queries, in one minute per query on average.