Transfer Function Synthesis without Quantifier Elimination

Brauer, Jorg and King, Andy (2011) Transfer Function Synthesis without Quantifier Elimination. In: Barthe, Gilles, ed. European Symposium on Programming. Lecture Notes in Computer Science, 6602 . Springer-Verlag, pp. 182-196. ISBN 978-3-642-19717-8. (Full text available)

PDF (Transfer Function Synthesis without Quantifier Elimination. ESOP 2011: 97-115)
Download (245kB) Preview
[img]
Preview
Official URL
http://www.cs.kent.ac.uk/pubs/2011/3072

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.

Item Type: Book section
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Programming Languages and Systems Group
Faculties > Science Technology and Medical Studies > School of Computing > Security Group
Depositing User: Andy King
Date Deposited: 21 Sep 2012 09:49
Last Modified: 12 Dec 2013 12:28
Resource URI: http://kar.kent.ac.uk/id/eprint/30765 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year