Brauer, Jorg and King, Andy (2011) Transfer Function Synthesis without Quantifier Elimination. In: Twentieth European Symposium on Programming.
|The full text of this publication is not available from this repository. (Contact us about this Publication)|
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:||Conference or workshop item (UNSPECIFIED)|
|Uncontrolled keywords:||determinacy analysis, Craig interpolants|
|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:||21 Sep 2012 09:49|
|Resource URI:||http://kar.kent.ac.uk/id/eprint/30765 (The current URI for this page, for reference purposes)|
- Depositors only (login required):