Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors

JONÁŠ, Martin a Jan STREJČEK. Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors. Online. In Isil Dillig, Serdar Tasiran. CAV 2019: Computer Aided Verification. Cham (Switzerland): Springer, 2019, s. 64-73. ISBN 978-3-030-25542-8. Dostupné z: https://dx.doi.org/10.1007/978-3-030-25543-5_4.

Základní údaje

Originální název

Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors

Autoři

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

Vydání

Cham (Switzerland), CAV 2019: Computer Aided Verification, od s. 64-73, 10 s. 2019

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/19:00107610

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-25542-8

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-25543-5_4

UT WoS

000491468900004

Klíčová slova anglicky

satisfiability; satisfiability modulo theories; bit-vectors; quantifiers; tool

Štítky

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

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

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