Skip to main content

Range and Set Abstraction using SAT

Barrett, Edd, King, Andy (2012) Range and Set Abstraction using SAT. Electronic Notes in Theoretical Computer Science, 267 (1). pp. 93-107. ISSN 978-3-642-32468-0. (doi:10.1016/j.entcs.2010.09.003) (KAR id:30621)

Language: English
Click to download this file (435kB) Preview
[thumbnail of main.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


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 bit-vectors 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 bit-vectors that are constrained by Boolean formulae.

Item Type: Article
DOI/Identification number: 10.1016/j.entcs.2010.09.003
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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: E. Barrett
Date Deposited: 21 Sep 2012 09:49 UTC
Last Modified: 16 Nov 2021 10:08 UTC
Resource URI: (The current URI for this page, for reference purposes)
King, Andy:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.