Transfer Function Synthesis Without Quantifier Elimination

Download Now Date Added: Jan 2011
Format: PDF

Recently it has been shown how transfer functions for linear template constraints can be derived for bit-vector programs by operating over propositional Boolean formulae. The drawback of this method is that it relies on existential quantifier elimination, which induces a computational bottleneck. The contribution of this paper is a novel method for synthesising transfer functions that does not rely on quantifier elimination. The authors demonstrate the practicality of the method for generating transfer functions for both intervals and octagons.