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

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní 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.