Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1552339,
author = {Jonáš, Martin and Strejček, Jan},
address = {Cham (Switzerland)},
booktitle = {CAV 2019: Computer Aided Verification},
doi = {http://dx.doi.org/10.1007/978-3-030-25543-5_4},
editor = {Isil Dillig, Serdar Tasiran},
keywords = {satisfiability; satisfiability modulo theories; bit-vectors; quantifiers; tool},
howpublished = {elektronická verze "online"},
language = {eng},
location = {Cham (Switzerland)},
isbn = {978-3-030-25542-8},
pages = {64-73},
publisher = {Springer},
title = {Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors},
url = {https://link.springer.com/chapter/10.1007%2F978-3-030-25543-5_4},
year = {2019}
}
TY - JOUR
ID - 1552339
AU - Jonáš, Martin - Strejček, Jan
PY - 2019
TI - Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
PB - Springer
CY - Cham (Switzerland)
SN - 9783030255428
KW - satisfiability
KW - satisfiability modulo theories
KW - bit-vectors
KW - quantifiers
KW - tool
UR - https://link.springer.com/chapter/10.1007%2F978-3-030-25543-5_4
N2 - We present the first stable release of our tool Q3B for deciding satisfiability of quantified bit-vector formulas. Unlike other state-of-the-art solvers for this problem, Q3B is based on translation of a formula to a bdd that represents models of the formula. The tool also employs advanced formula simplifications and approximations by effective bit-width reduction and by abstraction of bit-vector operations. The paper focuses on the architecture and implementation aspects of the tool, and provides a brief experimental comparison with its competitors.
ER -
JONÁŠ, Martin and Jan STREJČEK. Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors. Online. In Isil Dillig, Serdar Tasiran. \textit{CAV 2019: Computer Aided Verification}. Cham (Switzerland): Springer, 2019, p.~64-73. ISBN~978-3-030-25542-8. Available from: https://dx.doi.org/10.1007/978-3-030-25543-5\_{}4.
|
