Barrett, Edd and King, Andy (2012) Range and Set Abstraction using SAT. Electronic Notes in Theoretical Computer Science, 267 (1). pp. 93107. ISSN 9783642324680. (Full text available)
Download (391kB)
Preview



Official URL http://www.cs.kent.ac.uk/pubs/2010/3050 
Abstract
Symbolic decision trees are not the only way to correlate the relationship between flags and numeric variables. Boolean formulae can also represent such relationships where the integer variables are modelled with bitvectors of propositional variables. Boolean formulae can be composed to express the semantics of a block and program state, but they are hardly tractable, hence the need to compute their abstractions. This paper shows how incremental SAT can be applied to derive range and set abstractions for bitvectors that are constrained by Boolean formulae.
Item Type:  Article 

Uncontrolled keywords:  range analysis, interval analysis, binary analysis, linear optimisation 
Subjects:  Q Science > QA Mathematics (inc Computing science) > QA564 Algebraic Geometry Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics 
Divisions:  Faculties > Science Technology and Medical Studies > School of Computing > Programming Languages and Systems Group 
Depositing User:  E. Barrett 
Date Deposited:  21 Sep 2012 09:49 
Last Modified:  26 Sep 2012 13:36 
Resource URI:  http://kar.kent.ac.uk/id/eprint/30621 (The current URI for this page, for reference purposes) 
 Export to:
 RefWorks
 EPrints3 XML
 CSV
 Depositors only (login required):