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

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

JONÁŠ Martin STREJČEK Jan

Rok publikování 2019
Druh Článek ve sborníku
Konference CAV 2019: Computer Aided Verification
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www 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
Klíčová slova satisfiability; satisfiability modulo theories; bit-vectors; quantifiers; tool
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.