Refining static analyses by trace-based partitioning using control flow

Abstract

This paper presents a systematic method of building a more precise static analysis from a given one. The key idea is to lift an abstract domain to the finite sets of its labeled abstract properties. The labels are designed to gather information about the history of control flow and to obtain a finite partitioning of the program execution traces. The abstract operations of the lifted domain are derived from those of the original one. This is a particular instance of the reduced cardinal power introduced by P. and R. Cousot, where the base is the set of labels approximating the control history and the exponent is an abstract domain. The method is applied to the domain of convex polyhedra and to the domain of linear congruences. © 1998 Springer-Verlag Berlin Heidelberg.