Truncating abstraction of bit-vector operations for BDD-based
SMT solvers

J 2024

Truncating abstraction of bit-vector operations for BDD-based SMT solvers

JONÁŠ, Martin a Jan STREJČEK

Základní údaje

Originální název

Truncating abstraction of bit-vector operations for BDD-based SMT solvers

Autoři

JONÁŠ, Martin a Jan STREJČEK

Vydání

THEORETICAL COMPUTER SCIENCE, NETHERLANDS, ELSEVIER, 2024, 0304-3975

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

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

Odkazy

URL

Impakt faktor

Impact factor: 1.000

Kód RIV

RIV/00216224:14330/24:00139156

Organizační jednotka

Fakulta informatiky

DOI

https://doi.org/10.1016/J.TCS.2024.114664

UT WoS

001254826000001

EID Scopus

2-s2.0-85195574216

Klíčová slova anglicky

Bit-vector theory; Operation abstraction; Q3B; SMT solving

Štítky

bit-vector logic, formela-journal, satisfiability, SMT solving, verification

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 4. 4. 2025 12:43, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

During the last few years, BDD-based SMT solvers proved to be competitive in deciding satisfiability of quantified bit-vector formulas. However, these solvers usually do not perform well on input formulas with complicated arithmetic. Hitherto, this problem has been alleviated by approximations reducing effective bit-widths of bit-vector variables. In this paper, we propose an orthogonal abstraction technique that works 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 SMT solvers Boolector, CVC4, and Z3.

Návaznosti

GA23-06506S, projekt VaV

Název: Pokročilá analýza a verifikace pro pokročilý software

Investor: Grantová agentura ČR, Pokročilá analýza a verifikace pro pokročilý software

Citovat

JONÁŠ, Martin a Jan STREJČEK. Truncating abstraction of bit-vector operations for BDD-based SMT solvers. THEORETICAL COMPUTER SCIENCE. NETHERLANDS: ELSEVIER, 2024, roč. 1008, č. 114664, s. 1-22. ISSN 0304-3975. Dostupné z: https://doi.org/10.1016/J.TCS.2024.114664.

@article{2486497,
   author = {Jonáš, Martin and Strejček, Jan},
   article_location = {NETHERLANDS},
   article_number = {114664},
   doi = {https://doi.org/10.1016/J.TCS.2024.114664},
   keywords = {Bit-vector theory; Operation abstraction; Q3B; SMT solving},
   language = {eng},
   issn = {0304-3975},
   journal = {THEORETICAL COMPUTER SCIENCE},
   title = {Truncating abstraction of bit-vector operations for BDD-based SMT solvers},
   url = {https://doi.org/10.1016/j.tcs.2024.114664},
   volume = {1008},
   year = {2024}
}

TY  - JOUR
ID  - 2486497
AU  - Jonáš, Martin - Strejček, Jan
PY  - 2024
TI  - Truncating abstraction of bit-vector operations for BDD-based SMT solvers
JF  - THEORETICAL COMPUTER SCIENCE
VL  - 1008
IS  - 114664
SP  - 1-22
EP  - 1-22
PB  - ELSEVIER
SN  - 03043975
KW  - Bit-vector theory
KW  - Operation abstraction
KW  - Q3B
KW  - SMT solving
UR  - https://doi.org/10.1016/j.tcs.2024.114664
N2  - During the last few years, BDD-based SMT solvers proved to be competitive in deciding satisfiability of quantified bit-vector formulas. However, these solvers usually do not perform well on input formulas with complicated arithmetic. Hitherto, this problem has been alleviated by approximations reducing effective bit-widths of bit-vector variables. In this paper, we propose an orthogonal abstraction technique that works 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 SMT solvers Boolector, CVC4, and Z3.
ER  -

JONÁŠ, Martin a Jan STREJČEK. Truncating abstraction of bit-vector operations for BDD-based SMT solvers. \textit{THEORETICAL COMPUTER SCIENCE}. NETHERLANDS: ELSEVIER, 2024, roč.~1008, č.~114664, s.~1-22. ISSN~0304-3975. Dostupné z: https://doi.org/10.1016/J.TCS.2024.114664.

Přehled o publikaci