© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Transfer Function Synthesis without Quantifier Elimination
Jorg Brauer and Andy King
In Gilles Barthe, editor, Twentieth European Symposium on Programming, volume 6602 of Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, March 2011.Abstract
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.
Download publication 239 kbytes (PDF)Bibtex Record
@inproceedings{3072, author = {Jorg Brauer and Andy King}, title = {Transfer {F}unction {S}ynthesis without {Q}uantifier {E}limination}, month = {March}, year = {2011}, pages = {182-196}, keywords = {determinacy analysis, Craig interpolants}, note = {}, doi = {}, url = {http://www.cs.kent.ac.uk/pubs/2011/3072}, publication_type = {inproceedings}, submission_id = {23676_1292418244}, booktitle = {Twentieth European Symposium on Programming}, editor = {Gilles Barthe}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, refereed = {yes}, volume = {6602}, }