This paper addresses the problem of abstracting a set of affine transformers v' = v · C + d, where v and v' represent the pre-state and post-state, respectively. We introduce a framework to harness any base abstract domain ℬ in an abstract domain of affine transformations. Abstract domains are usually used to define constraints on the variables of a program. In this paper, however, abstract domain ℬ is re-purposed to constrain the elements of C and d—thereby defining a set of affine transformers on program states. This framework facilitates intra- and interprocedural analyses to obtain function and loop summaries, as well as to prove program assertions.

(Click here to access the paper: PDF; extended version with proofs; (c) Springer-Verlag.)