More Web Proxy on the site http://driver.im/

Article

Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic

Authors:

Rhishikesh Limaye,

Sanjit A. SeshiaAuthors Info & Claims

CAV '09: Proceedings of the 21st International Conference on Computer Aided Verification

Pages 668 - 674

https://doi.org/10.1007/978-3-642-02658-4_53

Published: 23 June 2009 Publication History

Abstract

We present the key ideas in the design and implementation of Beaver, an SMT solver for quantifier-free finite-precision bit-vector logic (QF_BV). Beaver uses an eager approach, encoding the original SMT problem into a Boolean satisfiability (SAT) problem using a series of word-level and bit-level transformations. In this paper, we describe the most effective transformations, such as propagating constants and equalities at the word-level, and using and-inverter graph rewriting techniques at the bit-level. We highlight implementation details of these transformations that distinguishes Beaver from other solvers. We present an experimental analysis of the effectiveness of Beaver's techniques on both hardware and software benchmarks with a selection of back-end SAT solvers.

Beaver is an open-source tool implemented in Ocaml, usable with any back-end SAT engine, and has a well-documented extensible code base that can be used to experiment with new algorithms and techniques.

References

[1]

Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, ch. 8, vol. 4. IOS Press, Amsterdam (2009).

[2]

Biere, A.: PicoSAT essentials. JSAT 4, 75-97 (2008).

[3]

Brummayer, R.D., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Proc. of TACAS (March 2009).

[4]

Bruttomesso, R., Cimatti, A., Franzen, A., Griggio, A., Hanna, Z., Nadel, A., Palti, A., Sebastiani, R.: A lazy and layered SMT(BV) solver for hard industrial verification problems. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 547-560. Springer, Heidelberg (2007).

[5]

Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 358-372. Springer, Heidelberg (2007).

[6]

de Moura, L., Bjorner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337-340. Springer, Heidelberg (2008).

[7]

Een, N., Sorensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502-518. Springer, Heidelberg (2004).

[8]

Ganesh, V., Dill, D.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519-531. Springer, Heidelberg (2007).

[9]

Hutter, F., Babic, D., Hoos, H.H., Hu, A.J.: Boosting verification by automatic tuning of decision procedures. In: FMCAD 2007, pp. 27-34. IEEE Press, Los Alamitos (2007).

[10]

Manolis, P., Srinivasan, S.K., Vroon, D.: BAT Bit-level Analysis tool. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 303-306. Springer, Heidelberg (2007).

[11]

Jain, H., Clarke, E.M.: Efficient SAT solving for Non-Clausal Formulas using DPLL, Graphs and Watched Cuts. In: 46th Design Automation Conference (2009).

[12]

Pipatsrisawat, K., Darwiche, A.: Rsat 2.0: Sat solver description. Technical Report D-153, Automated Reasoning Group, Computer Science Department, UCLA (2007).

[13]

SMT-COMP 2008 results, http://www.smtexec.org/exec/?jobs=311

[14]

SMT-LIB QF BV logic, http://goedel.cs.uiowa.edu/smtlib/logics/QF_BV.smt

[15]

SMT-LIB QF BV benchmarks, http://combination.cs.uiowa.edu/smtlib/benchmarks.html

[16]

Berkeley Logic Synthesis and Verification Group. ABC: A system for sequential synthesis and verification, release 70930, http://www.eecs.berkeley.edu/~alanmi/abc/

[17]

Jha, S., Limaye, R., Seshia, S.A.: Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic. Technical Report, EECS Department, UC Berkeley (April 2009).

[18]

Een, N., Mishchenko, A., Sorensson, N.: Applying logic synthesis to speedup SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 272-286. Springer, Heidelberg (2007).

[19]

Warren Jr., H.S.: Hacker's Delight. Addison Wesley, Reading (2003).

Cited By

VanHattum APardeshi MFallin CSampson ABrown FTsafrir DMUSUVATHI MGupta RAbu-Ghazaleh N(2024)Lightweight, Modular Verification for WebAssembly-to-Native Instruction SelectionProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3617232.3624862(231-248)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3617232.3624862
Kleine Büning MBalyo TSinz C(2019)Using DimSpec for Bounded and Unbounded Software Model CheckingFormal Methods and Software Engineering10.1007/978-3-030-32409-4_2(19-35)Online publication date: 5-Nov-2019
https://dl.acm.org/doi/10.1007/978-3-030-32409-4_2
Bataineh ORosenblum DReynolds M(2019)A Novel Decentralized LTL Monitoring Framework Using Formula Progression TableModel Checking Software10.1007/978-3-030-30923-7_3(38-55)Online publication date: 15-Jul-2019
https://dl.acm.org/doi/10.1007/978-3-030-30923-7_3
Show More Cited By

Recommendations

Small turing machines and generalized busy beaver competition

Let TM(k,l) be the set of one-tape Turing machines with k states and l symbols. It is known that the halting problem is decidable for machines in TM(2,3) and TM(3,2). We prove that the decidability of machines in TM(2,4) and TM(3,3) will be difficult to ...
Hardness of Busy Beaver Value BB(15)
Reachability Problems
Abstract
The busy beaver value BB(n) is the maximum number of steps made by any n-state, 2-symbol deterministic halting Turing machine starting on blank tape. The busy beaver function $n \mapsto BB (n)$ is uncomputable and, from below, only 4 of its values, $BB (1) \dots BB (...$ $^{}$
Analysis of busy beaver machines via induction proofs
CATS '07: Proceedings of the thirteenth Australasian symposium on Theory of computing - Volume 65

The busy beaver problem is to find the maximum number of 1's that can be printed by an n-state Turing machine of a particular type. A critical step in the evaluation of this value is to determine whether or not a given n-state Turing machine halts. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV '09: Proceedings of the 21st International Conference on Computer Aided Verification

June 2009

720 pages

ISBN:9783642026577

Editors:
Ahmed Bouajjani
LIAFA, University Paris Diderot (Paris 7), Case 7014, Paris Cedex 13, France 75205
,
Oded Maler
Verimag, Centre Equation, Gières, France 38610

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 23 June 2009

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 28 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

VanHattum APardeshi MFallin CSampson ABrown FTsafrir DMUSUVATHI MGupta RAbu-Ghazaleh N(2024)Lightweight, Modular Verification for WebAssembly-to-Native Instruction SelectionProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3617232.3624862(231-248)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3617232.3624862
Kleine Büning MBalyo TSinz C(2019)Using DimSpec for Bounded and Unbounded Software Model CheckingFormal Methods and Software Engineering10.1007/978-3-030-32409-4_2(19-35)Online publication date: 5-Nov-2019
https://dl.acm.org/doi/10.1007/978-3-030-32409-4_2
Bataineh ORosenblum DReynolds M(2019)A Novel Decentralized LTL Monitoring Framework Using Formula Progression TableModel Checking Software10.1007/978-3-030-30923-7_3(38-55)Online publication date: 15-Jul-2019
https://dl.acm.org/doi/10.1007/978-3-030-30923-7_3
Sharif HAbubakar MGehani AZaffar FHuchard MKästner CFraser G(2018)TRIMMER: application specialization for code debloatingProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3238160(329-339)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3238147.3238160
Borraz-Sánchez CKlabjan DPasalic EAref M(2018)SolverBloxDeclarative Logic Programming10.1145/3191315.3191322(331-354)Online publication date: 1-Sep-2018
https://dl.acm.org/doi/10.1145/3191315.3191322
Solé MCarmona J(2018)Encoding process discovery problems in SMTSoftware and Systems Modeling (SoSyM)10.1007/s10270-016-0536-y17:4(1055-1078)Online publication date: 1-Oct-2018
https://dl.acm.org/doi/10.1007/s10270-016-0536-y
Gupta SSaxena AMahajan ABansal S(2018)Effective Use of SMT Solvers for Program Equivalence Checking Through Invariant-Sketching and Query-DecompositionTheory and Applications of Satisfiability Testing – SAT 201810.1007/978-3-319-94144-8_22(365-382)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.1007/978-3-319-94144-8_22
Braione PDenaro GMattavelli APezzè MBultan TSen K(2017)Combining symbolic execution and search-based testing for programs with complex heap inputsProceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3092703.3092715(90-101)Online publication date: 10-Jul-2017
https://dl.acm.org/doi/10.1145/3092703.3092715
Chakraborty SKhasidashvili ZSeger CGajavelly RHaldankar TChhatani DMistry R(2017)Symbolic trajectory evaluation for word-level verificationFormal Methods in System Design10.1007/s10703-017-0268-950:2-3(317-352)Online publication date: 1-Jun-2017
https://dl.acm.org/doi/10.1007/s10703-017-0268-9
Chakraborty SMeel KMistry RVardi M(2016)Approximate probabilistic inference via word-level countingProceedings of the Thirtieth AAAI Conference on Artificial Intelligence10.5555/3016100.3016354(3218-3224)Online publication date: 12-Feb-2016
https://dl.acm.org/doi/10.5555/3016100.3016354
Show More Cited By

View Options

View options

Figures

Tables

Media

View Table of Conten