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

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

JONÁŠ Martin STREJČEK Jan

Year of publication 2019
Type Article in Proceedings
Conference CAV 2019: Computer Aided Verification
MU Faculty or unit

Faculty of Informatics

Citation
Web https://link.springer.com/chapter/10.1007%2F978-3-030-25543-5_4
Doi http://dx.doi.org/10.1007/978-3-030-25543-5_4
Keywords satisfiability; satisfiability modulo theories; bit-vectors; quantifiers; tool
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.