Program
Verification
Book

PV4 ⊧ Q3Bproduces a satisfiability result for a formula

SMT solver, decides satisfiability of quantified bit-vector formulas.

Application domain/field

SMT solving
Quantified bit-vector formulas
Binary Decision Diagrams (BDDs)

Type of tool

SMT solver

Expected input

Quantified bit-vector formula

Format:

SMT-LIB 2.5

Expected output

sat or unsat indicating whether the quantified bit-vector formula was satisfiable or not.

Internals

Uses CUDD, ANTLR, SMT-LIB, Z3

Links

Repository: https://github.com/martinjonas/Q3B

Last commit date: 06 Mar 2019 (default branch)
Last commit date: 02 Jul 2022 (last activity)

Related papers

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

Last publication date

12 July 2019

ProVerB specific

Markdown description: view/edit
Reason for this entry: CAV 2019
Contained in the ProVerB22 dataset (paper + artefact)

ProVerB is a part of SLEBoK. Last updated: February 2023.