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

D 2018

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

JONÁŠ, Martin a Jan STREJČEK

Základní údaje

Originální název

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

Autoři

JONÁŠ, Martin (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

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

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/18:00101330

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-02507-6

ISSN

DOI

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

UT WoS

000612998900015

Klíčová slova anglicky

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

Štítky

core_B, firank_B, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 29. 4. 2019 15:23, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

GA18-02177S, projekt VaV

Název: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Grantová agentura ČR, Abstrakce a jiné techniky v semi-symbolické verifikaci programů

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

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

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

JONÁŠ, Martin a 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, s. 273-291. ISBN 978-3-030-02507-6. Dostupné z: 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 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.

Podrobný výpis o publikaci