Detailed Information on Publication Record
2019
Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
JONÁŠ, Martin and Jan STREJČEKBasic information
Original name
Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
Authors
JONÁŠ, Martin (203 Czech Republic, belonging to the institution) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)
Edition
Cham (Switzerland), CAV 2019: Computer Aided Verification, p. 64-73, 10 pp. 2019
Publisher
Springer
Other information
Language
English
Type of outcome
Stať ve sborníku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Switzerland
Confidentiality degree
není předmětem státního či obchodního tajemství
Publication form
electronic version available online
References:
Impact factor
Impact factor: 0.402 in 2005
RIV identification code
RIV/00216224:14330/19:00107610
Organization unit
Faculty of Informatics
ISBN
978-3-030-25542-8
ISSN
UT WoS
000491468900004
Keywords in English
satisfiability; satisfiability modulo theories; bit-vectors; quantifiers; tool
Tags
International impact, Reviewed
Změněno: 28/4/2020 07:44, RNDr. Pavel Šmerk, Ph.D.
Abstract
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.
Links
| GA18-02177S, research and development project |
| ||
| MUNI/A/1018/2018, interní kód MU |
| ||
| MUNI/A/1040/2018, interní kód MU |
|