The Quantified Boolean Formulas Satisfiability Library
Home
Instances
Solvers
QBF Evaluations
Application domain Formal Verification
Description:
Number of families:
66
Families:
Adder (
32
)
amba (
56
)
blackbox-01X-QBF (
450
)
blackbox_design (
28
)
Bloem_dqbf (
174
)
BMC (
132
)
C432 (
8
)
C499 (
8
)
C5315 (
8
)
C6288 (
8
)
C880 (
8
)
circuits (
63
)
comp (
8
)
Counter (
88
)
cycle-sched (
78
)
Debug (
38
)
DFlipFlop (
10
)
driver (
38
)
FPGA_PLB_FIT_FAST (
5
)
FPGA_PLB_FIT_SLOW (
3
)
fpu (
398
)
genbuf (
115
)
HardwareFixpoint (
131
)
hwmcc (
110
)
incrementer-encoder (
612
)
irqlkeapclte (
46
)
ISCAS89 (
408
)
ITC99 (
519
)
jctc (
17
)
jmc_quant (
10
)
jmc_quant_squaring (
10
)
LinearBitvectorRankingFunction (
60
)
ltl2aig-comp (
56
)
LTL2DBA (
32
)
mult-matrix (
510
)
MutexP (
7
)
NuSMV_diam (
92
)
NuSMV_diam_bin (
92
)
qbfeval12 (
17
)
QLTL_safety (
500
)
RankingFunctions (
372
)
s1196 (
6
)
s1269 (
14
)
s27 (
4
)
s298 (
24
)
s3271 (
8
)
s3330 (
13
)
s386 (
11
)
s499 (
25
)
s510 (
50
)
s641 (
9
)
s713 (
10
)
s820 (
14
)
Scholl_dqbf (
150
)
SzymanskiP (
12
)
Tentrup_dqbf (
118
)
term1 (
8
)
terminator (
595
)
tipdiam (
203
)
tipfixpoint (
446
)
toy (
259
)
trafficlight-controller (
1622
)
uclid (
3
)
VonNeumann (
11
)
wmiforward (
72
)
z4ml (
8
)
Results:
Contact
|
Organization
|
Links
|
Citing QBFLIB