Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(13)
Automated Theorem Proving
Blow Up
Decision Procedure
Hardware Design
Hardware Synthesis
Integrated Circuit
Ranking Function
Sat Solver
Satisfiability
Software Design
Software Verification
Theorem Prover
Quantified Boolean Formula
Subscribe
Academic
Publications
Efficiently solving quantified bitvector formulas
Efficiently solving quantified bitvector formulas,Christoph M. Wintersteiger,Youssef Hamadi,Leonardo Mendonça de Moura
Edit
Efficiently solving quantified bitvector formulas
(
Citations: 4
)
BibTex

RIS

RefWorks
Download
Christoph M. Wintersteiger
,
Youssef Hamadi
,
Leonardo Mendonça de Moura
In recent years, bitprecise 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 quantifierfree fragment of bitvector logic exist and often rely on SAT solvers for efficiency. However, many techniques require quantifiers in bitvector for mulas to avoid an exponential blowup during construction. Solvers for quantified formulas usually flatten the input to obtain a quantified Boolean formula, losing much of the wordlevel information in the formula. We present a new approach based on a set of effective wordlevel 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, bitprecise 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 lowlevel 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 errordescription (27) are all instances of the general synthesis problem. In this paper, we present a new approach to solving quanti fied bitvector logic. This logic allows for a direct mapping of hardware and (finitestate)
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 bitvector 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 ComputerAided Design  FMCAD
, pp. 239246, 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.
(
research.microsoft.com
)
(
www.winterstiger.at
)
(
research.microsoft.com
)
(
ieeexplore.ieee.org
)
(
ieeexplore.ieee.org
)
(
www.informatik.unitrier.de
)
More »
Citation Context
(4)
...In particular, the theory of bitvectors with uninterpreted functions and quantiers (SMT UFBV) has been shown to be a very eective means of analyzing BMC instances [
33
]...
Josh Berdine
,
et al.
Diagnosing Abstraction Failure for Separation Logicbased Analyses
...The use of such theories is attractive due to recently developed quantied bitvector formula procedures [
77
]...
Boyan Yordanov
,
et al.
SMTbased analysis of biological computation
...A recent contribution to reasoning about quantified bitvector formulae was made by Wintersteiger et al. [
36
], who most notably used wordlevel 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 Brauer
,
et 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 bitvector 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 bitvector 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 counterexampleguided 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áš Janota
,
et al.
AbstractionBased Algorithm for 2QBF
References
(27)
CVC3
(
Citations: 29
)
Clark Barrett
,
Cesare Tinelli
Conference:
Computer Aided Verification  CAV
, pp. 298302, 2007
Evaluating QBFs via Symbolic Skolemization
(
Citations: 33
)
Marco Benedetti
Conference:
Logic Programming and Automated Reasoning/Russian Conference on Logic Programming  LPAR(RCLP)
, pp. 285300, 2004
Resolve and Expand
(
Citations: 122
)
Armin Biere
Conference:
Theory and Applications of Satisfiability Testing
, pp. 5970, 2004
Boolector: An Efficient SMT Solver for BitVectors and Arrays
(
Citations: 31
)
Robert Brummayer
,
Armin Biere
Conference:
Tools and Algorithms for Construction and Analysis of Systems  TACAS
, pp. 174177, 2009
Ranking Function Synthesis for BitVector Relations
(
Citations: 8
)
Byron Cook
,
Daniel Kroening
,
Philipp Rümmer
,
Christoph M. Wintersteiger
Conference:
Tools and Algorithms for Construction and Analysis of Systems  TACAS
, pp. 236250, 2010
Sort by:
Citations
(4)
Diagnosing Abstraction Failure for Separation Logicbased Analyses
Josh Berdine
,
Arlen Cox
,
Samin Ishtiaq
,
Christoph M. Wintersteiger
Published in 2012.
SMTbased analysis of biological computation
Boyan Yordanov
,
Christoph M. Wintersteiger
,
Youssef Hamadi
,
Hillel Kugler
Published in 2012.
Approximate Quantifier Elimination for Propositional Boolean Formulae
(
Citations: 1
)
Jörg Brauer
,
Andy King
Published in 2011.
AbstractionBased Algorithm for 2QBF
Mikoláš Janota
,
Joao MarquesSilva