School of Computing

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},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014