CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver.

Xiaomu Shi Yu-Fu Fu Jiaxiang Liu Ming-Hsien Tsai Bow-Yaw Wang Bo-Yin Yang

Published in: CAV (2) (2021)

Keyphrases

bit vector
quantifier free
quantifier elimination
satisfiability modulo theories
rewrite systems
first order logic
boolean formula
real numbers
relational data model
database
constraint propagation
constraint solver
np hard
constraint databases
functional programming