Další formáty:
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 a 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, s.~273-291. ISBN~978-3-030-02507-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-02508-3\_{}15.
|