PV2 CoqQFBVproduces a satisfiability formula for a query

SMT solver for QF_BV (quantifier-free bit-vector) logic.

Application domain/field

Type of tool

SMT solver for QF_BV logic

Expected input

SMT QF_BV query



Expected output

Boolean formula such that the query is satisfiable if and only if the Boolean formula is satisfiable. Output is generated in the DIMACS format.


This is a certified SMT solver for quantifier-free bit-vector (QF_BV) formulas. It has been specified and verified in the proof assistant Coq. It takes a QF_BV query in SMT-LIB format. This is converted into a formal QF_BV expression. Then a CNF formula is constructed. Then it uses Kissat to solve the CNF formula. If the result is unsat with a certificate, then the certificate is verified with GRAT. If the results is sat with assignments, then this is translated back to SMT assignments and the tool will verify whether these assignments satisfy the QF_BV expression.


Repository: https://github.com/fmlab-iis/coq-qfbv

Related papers

CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver (CAV '21)

Last publication date

15 July 2021

Related tools

Boolector, Bitwuzla, CVC4

ProVerB specific

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