Další formáty:
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 a 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, s.~64-73. ISBN~978-3-030-25542-8. Dostupné z: https://dx.doi.org/10.1007/978-3-030-25543-5\_{}4.
|