Record Details

NOPR - NISCAIR Online Periodicals Repository

View Archive Info
 
 
Field Value
 
Title A layered algorithm for quantifier elimination from linear modular constraints
 
##plugins.schemas.dc.fields.names.name## Array
Array
 
##plugins.schemas.dc.fields.originInfo.name## Array
 
##plugins.schemas.dc.fields.genre.name## Article
 
Abstract Linear equalities, disequalities and inequalities on fixed-width bit-vectors, collectively called linear modular constraints, form an important fragment of the theory of fixed-width bit-vectors. We present a practically efficient and bit-precise algorithm for quantifier elimination from conjunctions of linear modular constraints. Our algorithm uses a layered approach, whereby sound but incomplete and cheaper layers are invoked first, and expensive but complete layers are called only when required. We then extend this algorithm to work with arbitrary Boolean combinations of linear modular constraints as well. Experiments on an extensive set of benchmarks demonstrate that our techniques significantly outperform alternative quantifier elimination techniques based on bit-blasting and linear integer arithmetic.
 
##plugins.schemas.dc.fields.extension.name##
 
Identifier FORMAL METHODS IN SYSTEM DESIGN,49(3)272-323
 
##plugins.schemas.dc.fields.identifierType.name## citation