Book chapter
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors
Computer Aided Verification, pp.680-695
Lecture Notes in Computer Science, Springer International Publishing
2014
DOI: 10.1007/978-3-319-08867-9_45
Abstract
The standard method for deciding bit-vector constraints is via eager reduction to propositional logic. This is usually done after first applying powerful rewrite techniques. While often efficient in practice, this method does not scale on problems for which top-level rewrites cannot reduce the problem size sufficiently. A lazy solver can target such problems by doing many satisfiability checks, each of which only reasons about a small subset of the problem. In addition, the lazy approach enables a wide range of optimization techniques that are not available to the eager approach. In this paper we describe the architecture and features of our lazy solver (LBV). We provide a comparative analysis of the eager and lazy approaches, and show how they are complementary in terms of the types of problems they can efficiently solve. For this reason, we propose a portfolio approach that runs a lazy and eager solver in parallel. Our empirical evaluation shows that the lazy solver can solve problems none of the eager solvers can and that the portfolio solver outperforms other solvers both in terms of total number of problems solved and the time taken to solve them.
Details
- Title: Subtitle
- A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors
- Creators
- Liana Hadarean - New York UniversityKshitij Bansal - New York UniversityDejan Jovanović - SRI InternationalClark Barrett - New York UniversityCesare Tinelli - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Computer Aided Verification, pp.680-695
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-319-08867-9_45
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 2014
- Academic Unit
- Computer Science
- Record Identifier
- 9984259403702771
Metrics
4 Record Views