D
2019
Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
JONÁŠ, Martin a Jan STREJČEK
Základní údaje
Originální název
Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
Vydání
Cham (Switzerland), CAV 2019: Computer Aided Verification, od s. 64-73, 10 s. 2019
Další údaje
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"
Impakt faktor
Impact factor: 0.402 v roce 2005
Kód RIV
RIV/00216224:14330/19:00107610
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
satisfiability; satisfiability modulo theories; bit-vectors; quantifiers; tool
Příznaky
Mezinárodní význam, Recenzováno
V originále
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.
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/1018/2018, interní kód MU | Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII. | Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty |
|
MUNI/A/1040/2018, interní kód MU | Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 19 (Akronym: SKOMU) | Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 19, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty |
|
Zobrazeno: 11. 11. 2024 02:00