Other formats:
BibTeX
LaTeX
RIS
@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. Online. 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. [citováno 2024-04-24]
|
