Environment Unrolling

Abstract. We propose a new way of thinking about abstract interpre-tation with a method we term environment unrolling. Model checkers for imperative languages will often apply loop unrolling to make their state space finite in the presence of loops and recursion. We propose handling environments in a similar fashion by putting a bound on the number of environments to which a given closure can transitively refer. We present how this idea relates to a normal model of abstract interpretation, give a general overview of its soundness proof in regards to a concrete seman-tics, and show empirical results demonstrating the effectiveness of our approach.