School of Computing

Range and Set Abstraction using SAT

Edd Barrett and Andy King

Electronic Notes in Theoretical Computer Science, 267(1):17-27, October 2010 [doi].

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 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.

Download publication 174 kbytes (PDF)

Bibtex Record

@article{3050,
author = {Edd Barrett and Andy King},
title = {Range and {S}et {A}bstraction using {SAT} },
month = {October},
year = {2010},
pages = {17-27},
keywords = {Abstract domains, Numeric domains, Ranges, Satisfiability solving.},
note = {},
doi = {10.1016/j.entcs.2010.09.003},
url = {http://www.cs.kent.ac.uk/pubs/2010/3050},
    publication_type = {article},
    submission_id = {28701_1287396574},
    journal = {Electronic Notes in Theoretical Computer Science},
    volume = {267},
    number = {1},
    publisher = {Elsevier},
}

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

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

Last Updated: 12/03/2012 17:31