Academic
Publications
Efficiently solving quantified bit-vector formulas

Efficiently solving quantified bit-vector formulas,Christoph M. Wintersteiger,Youssef Hamadi,Leonardo Mendonça de Moura

Efficiently solving quantified bit-vector formulas   (Citations: 4)
BibTex | RIS | RefWorks Download
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 for- mulas 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. I. INTRODUCTION The complexity of integrated circuits continues to grow at an exponential rate and so does the size of the verification and synthesis problems arising from the hardware design process. To tackle these problems, bit-precise decision procedures are a requirement and oftentimes the crucial ingredient that defines the efficency of the verification process. Recent years also saw an increase in the utility of bit- precise reasoning in the area of software verification where low-level languages like C or C++ are concerned. In both areas, hardware and software design, methods of automated synthesis (e.g., LTL synthesis (23)) become more and more tangible with the advent of powerful and efficient decision procedures for various logics, most notably SAT and SMT solvers. In practice, however, synthesis methods are often incomplete, bound to very specific application domains, or simply inefficient. In the case of hardware, synthesis usually amounts to constructing a module that implements a specification (23), (20), while for software this can take different shapes: inferring program invariants (16), finding ranking functions for termina- tion analysis (28), (24), (8), program fragment synthesis (26), or constructing bugfixes following an error-description (27) are all instances of the general synthesis problem. In this paper, we present a new approach to solving quanti- fied bit-vector logic. This logic allows for a direct mapping of hardware and (finite-state) software verification problems and is thus ideally suited as an interface between the verification or synthesis tool and the decision procedure. In many practically relevant applications, support for un- interpreted functions is not required and if this is the case, quantified bit-vector formulas can be reduced to quantified Boolean formulas (QBF). In practice however, QBF solvers face performance problems and they are usually not able to produce models for satisfiable formulas, which is crucial in synthesis applications. The same holds true for many automated theorem provers. SMT solvers on the other hand are efficient and produce models, but usually lack complete support for quantifiers. The ideas in this paper combine techniques from automated theorem proving, SMT solving and synthesis algorithms. We propose a set of simplifications and rewriting techniques that transform the input into a set of equations that an SMT solver is able to solve efficiently. A model finding algorithm is then employed to refine a candidate model iteratively, while we use function or circuit templates to reduce the number of iterations required by the algorithm. Finally, we evalutate a prototype implementation of our algorithm on a set of hardware and software benchmarks, which indicate speedups of up to five orders of magnitude compared to flattening the input to QBF.
Conference: Formal Methods in Computer-Aided Design - FMCAD , pp. 239-246, 2010
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...In particular, the theory of bit-vectors with uninterpreted functions and quantiers (SMT UFBV) has been shown to be a very eective means of analyzing BMC instances [33]...

    Josh Berdineet al. Diagnosing Abstraction Failure for Separation Logic--based Analyses

    • ...The use of such theories is attractive due to recently developed quantied bit-vector formula procedures [77]...

    Boyan Yordanovet al. SMT-based analysis of biological computation

    • ...A recent contribution to reasoning about quantified bit-vector formulae was made by Wintersteiger et al. [36], who most notably used word-level simplifications and template instantiations...
    • ...Future Work. This work calls for further investigations of ways to reduce the number of spurious candidates that appear when implicants of negations are enumerated, possibly based on the recent work described in [36]...

    Jörg Braueret al. Approximate Quantifier Elimination for Propositional Boolean Formulae

    • ...Moreover, recent work has applied the CEGAR paradigm in handling quantification on a number of different settings with promising results, including propositional circumscription [20], quantified bit-vector formulas [40], and linear real arithmetic [26]...
    • ...More recently, there has been increased interest in the CEGAR approach in the context of quantification [20,40,26]...
    • ...Finally, the work reported in [40] is solving a computationally harder decision problem, namely quantified bit-vector formulas...
    • ...This means that [40] can be used to solve arbitrary QBFs, but it is also unlikely to scale as well as a dedicated algorithm...
    • ...Although the work builds on recent work on using counterexample-guided abstraction for handling quantification [20,40,26], the algorithm exploits the natural properties of the problem formulation, and is shown to outperform approaches based on mapping QBF to another domain [20]...

    Mikoláš Janotaet al. Abstraction-Based Algorithm for 2QBF

Sort by: