Efficiently Solving Quantified Bit-Vector Formulas

Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo de Moura

Abstract

In recent years, bit-precise reasoning has gained importance in hardware and software verification. Of renewed interest is the use of symbolic reasoning for synthesising loop invariants, ranking functions, or whole program fragments and hardware circuits. Solvers for the quantifier-free fragment of bit-vector logic exist and often rely on SAT solvers for efficiency. However, many techniques require quantifiers in bit-vector formulas to avoid an exponential blow-up during construction. Solvers for quantified formulas usually flatten the input to obtain a quantified Boolean formula, losing much of the word-level information in the formula. We present a new approach based on a set of effective word-level simplifications that are traditionally employed in automated theorem proving, heuristic quantifier instantiation methods used in SMT solvers, and model finding techniques based on skeletons/templates. Experimental results on two different types of benchmarks indicate that our method outperforms the traditional flattening approach by multiple orders of magnitude of runtime.

Details

Publication typeArticle
Published inFormal Methods in System Design
Pages3-23
Volume42
Number1
PublisherSpringer
> Publications > Efficiently Solving Quantified Bit-Vector Formulas