Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width
Reductions and Extensions

D 2020

Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions

JONÁŠ, Martin a Jan STREJČEK

Základní údaje

Originální název

Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions

Autoři

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

Vydání

Cham (Switzerland), Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, od s. 378-393, 16 s. 2020

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í

elektronická verze "online"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/20:00114392

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-51824-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-51825-7_27

UT WoS

000711645300027

Klíčová slova anglicky

SMT solving; bit-vector logic; Boolector; Q3B

Štítky

bit-vector logic, core_A, firank_A, formela-conference, SMT solving

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 29. 4. 2021 12:29, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Recent experiments have shown that satisfiability of a quantified bit-vector formula coming from practical applications almost never changes after reducing all bit-widths in the formula to a small number of bits. This paper proposes a novel technique based on this observation. Roughly speaking, a given quantified bit-vector formula is reduced and sent to a solver, an obtained model is then extended to the original bit-widths and verified against the original formula. We also present an experimental evaluation demonstrating that this technique can significantly improve the performance of state-of-the-art smt solvers Boolector, CVC4, and Q3B on quantified bit-vector formulas from the smt-lib repository.

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ů

Citovat

JONÁŠ, Martin a Jan STREJČEK. Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. Online. In Luca Pulina and Martina Seidl. Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings. Cham (Switzerland): Springer, 2020, s. 378-393. ISBN 978-3-030-51824-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-51825-7_27.

@inproceedings{1686869,
   author = {Jonáš, Martin and Strejček, Jan},
   address = {Cham (Switzerland)},
   booktitle = {Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings},
   doi = {http://dx.doi.org/10.1007/978-3-030-51825-7_27},
   editor = {Luca Pulina and Martina Seidl},
   keywords = {SMT solving; bit-vector logic; Boolector; Q3B},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Switzerland)},
   isbn = {978-3-030-51824-0},
   pages = {378-393},
   publisher = {Springer},
   title = {Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions},
   url = {https://link.springer.com/chapter/10.1007%2F978-3-030-51825-7_27},
   year = {2020}
}

TY  - JOUR
ID  - 1686869
AU  - Jonáš, Martin - Strejček, Jan
PY  - 2020
TI  - Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions
PB  - Springer
CY  - Cham (Switzerland)
SN  - 9783030518240
KW  - SMT solving
KW  - bit-vector logic
KW  - Boolector
KW  - Q3B
UR  - https://link.springer.com/chapter/10.1007%2F978-3-030-51825-7_27
L2  - https://link.springer.com/chapter/10.1007%2F978-3-030-51825-7_27
N2  - Recent experiments have shown that satisfiability of a quantified bit-vector formula coming from practical applications almost never changes after reducing all bit-widths in the formula to a small number of bits. This paper proposes a novel technique based on this observation. Roughly speaking, a given quantified bit-vector formula is reduced and sent to a solver, an obtained model is then extended to the original bit-widths and verified against the original formula. We also present an experimental evaluation demonstrating that this technique can significantly improve the performance of state-of-the-art smt solvers Boolector, CVC4, and Q3B on quantified bit-vector formulas from the smt-lib repository.
ER  -

JONÁŠ, Martin a Jan STREJČEK. Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. Online. In Luca Pulina and Martina Seidl. \textit{Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings}. Cham (Switzerland): Springer, 2020, s.~378-393. ISBN~978-3-030-51824-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-51825-7\_{}27.

Podrobný výpis o publikaci