Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers

D 2018

Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers

JONÁŠ, Martin and Jan STREJČEK

Basic information

Original name

Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers

Authors

JONÁŠ, Martin (203 Czech Republic, belonging to the institution) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

Cham (Switzerland), Theoretical Aspects of Computing – ICTAC 2018, p. 273-291, 19 pp. 2018

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/18:00101330

Organization unit

Faculty of Informatics

ISBN

978-3-030-02507-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-02508-3_15

UT WoS

000612998900015

Keywords in English

satisfiability modulo theories; binary decision diagrams; abstractions; bit-vectors

Abstract

V originále

BDD-based SMT solvers have recently shown to be competitive for solving satisfiability of quantified bit-vector formulas. However, these solvers reach their limits when the input formula contains complicated arithmetic. Hitherto, this problem has been alleviated by approximations reducing efficient bit-widths of bit-vector variables. In this paper, we propose an orthogonal abstraction technique working on the level of the individual instances of bit-vector operations. In particular, we compute only several bits of the operation result, which may be sufficient to decide the satisfiability of the formula. Experimental results show that our BDD-based SMT solver Q3B extended with these abstractions can solve more quantified bit-vector formulas from the smt-lib repository than state-of-the-art SMT solvers Boolector, CVC4, and Z3.

Links

GA18-02177S, research and development project

Name: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Czech Science Foundation

MUNI/A/0854/2017, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.

Investor: Masaryk University, Category A

Citovat

JONÁŠ, Martin and Jan STREJČEK. Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers. In Bernd Fischer, Tarmo Uustalu. Theoretical Aspects of Computing – ICTAC 2018. Cham (Switzerland): Springer, 2018, p. 273-291. ISBN 978-3-030-02507-6. Available from: https://dx.doi.org/10.1007/978-3-030-02508-3_15.

@inproceedings{1463058,
   author = {Jonáš, Martin and Strejček, Jan},
   address = {Cham (Switzerland)},
   booktitle = {Theoretical Aspects of Computing – ICTAC 2018},
   doi = {http://dx.doi.org/10.1007/978-3-030-02508-3_15},
   editor = {Bernd Fischer, Tarmo Uustalu},
   keywords = {satisfiability modulo theories; binary decision diagrams; abstractions; bit-vectors},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham (Switzerland)},
   isbn = {978-3-030-02507-6},
   pages = {273-291},
   publisher = {Springer},
   title = {Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers},
   url = {https://link.springer.com/chapter/10.1007/978-3-030-02508-3_15},
   year = {2018}
}

TY  - JOUR
ID  - 1463058
AU  - Jonáš, Martin - Strejček, Jan
PY  - 2018
TI  - Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers
PB  - Springer
CY  - Cham (Switzerland)
SN  - 9783030025076
KW  - satisfiability modulo theories
KW  - binary decision diagrams
KW  - abstractions
KW  - bit-vectors
UR  - https://link.springer.com/chapter/10.1007/978-3-030-02508-3_15
N2  - BDD-based SMT solvers have recently shown to be competitive for solving satisfiability of quantified bit-vector formulas. However, these solvers reach their limits when the input formula contains complicated arithmetic. Hitherto, this problem has been alleviated by approximations reducing efficient bit-widths of bit-vector variables. In this paper, we propose an orthogonal abstraction technique working on the level of the individual instances of bit-vector operations. In particular, we compute only several bits of the operation result, which may be sufficient to decide the satisfiability of the formula. Experimental results show that our BDD-based SMT solver Q3B extended with these abstractions can solve more quantified bit-vector formulas from the smt-lib repository than state-of-the-art SMT solvers Boolector, CVC4, and Z3.
ER  -

JONÁŠ, Martin and Jan STREJČEK. Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers. In Bernd Fischer, Tarmo Uustalu. \textit{Theoretical Aspects of Computing – ICTAC 2018}. Cham (Switzerland): Springer, 2018, p.~273-291. ISBN~978-3-030-02507-6. Available from: https://dx.doi.org/10.1007/978-3-030-02508-3\_{}15.

Detailed Information on Publication Record