Verified Systems International GmbH
Quality Assurance for Embedded Systems
Quality Assurance for Embedded Systems
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. We demonstrate the practicality of the method for generating transfer functions for both intervals and octagons.
Jörg Brauer, Andy King: Transfer Function Synthesis without Quantifier Elimination. In Logical Methods in Computer Science (Special Issue on ESOP 2011), 2012.