Transfer Function Synthesis without Quantifier Elimination

Traditionally, transfer functions have been designed manually for eachoperation in a program, instruction by instruction. In such a setting, atransfer function describes the semantics of a single instruction, detailinghow a given abstract input state is mapped to an abstract output state. The neteffect of a sequence of instructions, a basic block, can then be calculated bycomposing the transfer functions of the constituent instructions. However,precision can be improved by applying a single transfer function that capturesthe semantics of the block as a whole. Since blocks are program-dependent, thisapproach necessitates automation. There has thus been growing interest incomputing transfer functions automatically, most notably using techniques basedon quantifier elimination. Although conceptually elegant, quantifierelimination inevitably induces a computational bottleneck, which limits theapplicability of these methods to small blocks. This paper contributes a methodfor calculating transfer functions that finesses quantifier eliminationaltogether, and can thus be seen as a response to this problem. Thepracticality of the method is demonstrated by generating transfer functions forinput and output states that are described by linear template constraints,which include intervals and octagons.Comment: 37 pages, extended version of ESOP 2011 pape