Range and Set Abstraction using SAT

d Set Abstraction using SAT Edd Barrett Andy King School of Computing, University of Kent, CT2 7NF, UK 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 formula can be composed to express the semantics of a block and program state, but they are hardly tractable, hence the need to their abstractions. This paper shows how incremental SAT can be applied to derive range abstractions for bit-vectors that are constrained by Boolean formulae.

• Type: Journal
• Year: 2010
• Where: ENTCS
• Authors: Edd Barrett, Andy King
• Keywords: Abstractions, Barrett Andy King, ENTCS 2010, Software Engineering, UK Symbolic Decision