The Quantified Boolean Formulas Satisfiability Library
Home
Instances
Solvers
QBF Evaluations
Detail page for BMC family
Download (210944 Kb)
Submitter:
Hratch Mangassarian
Suite:
Mangassarian-Veneris
Domain:
Formal Verification
Description:
The BMC family consists of instances of Bounded Model Checking, where different properties are being checked for several circuits and different bounds.
Number of instances:
132
Results:
2020 - Track 1
2019 - Track 1
2018 - Track 1
2018 - Track 5
2017 - Track 1
2017 - Track 2
2016 - Track 1
2016 - Track 2
2016 - Track 5
2016 - Track 6
2016 - Track 7
2010 - Track 1
2008 - Track 1
2007 - Track 1
Instances:
c1_BMC_p1_k1024
c1_BMC_p1_k128
c1_BMC_p1_k16
c1_BMC_p1_k2
c1_BMC_p1_k2048
c1_BMC_p1_k256
c1_BMC_p1_k32
c1_BMC_p1_k4
c1_BMC_p1_k512
c1_BMC_p1_k64
c1_BMC_p1_k8
c1_BMC_p2_k1024
c1_BMC_p2_k128
c1_BMC_p2_k16
c1_BMC_p2_k2
c1_BMC_p2_k2048
c1_BMC_p2_k256
c1_BMC_p2_k32
c1_BMC_p2_k4
c1_BMC_p2_k512
c1_BMC_p2_k64
c1_BMC_p2_k8
c2_BMC_p1_k1024
c2_BMC_p1_k128
c2_BMC_p1_k16
c2_BMC_p1_k2
c2_BMC_p1_k2048
c2_BMC_p1_k256
c2_BMC_p1_k32
c2_BMC_p1_k4
c2_BMC_p1_k512
c2_BMC_p1_k64
c2_BMC_p1_k8
c2_BMC_p2_k1024
c2_BMC_p2_k128
c2_BMC_p2_k16
c2_BMC_p2_k2
c2_BMC_p2_k2048
c2_BMC_p2_k256
c2_BMC_p2_k32
c2_BMC_p2_k4
c2_BMC_p2_k512
c2_BMC_p2_k64
c2_BMC_p2_k8
c3_BMC_p1_k1024
c3_BMC_p1_k128
c3_BMC_p1_k16
c3_BMC_p1_k2
c3_BMC_p1_k2048
c3_BMC_p1_k256
c3_BMC_p1_k32
c3_BMC_p1_k4
c3_BMC_p1_k512
c3_BMC_p1_k64
c3_BMC_p1_k8
c3_BMC_p2_k1024
c3_BMC_p2_k128
c3_BMC_p2_k16
c3_BMC_p2_k2
c3_BMC_p2_k2048
c3_BMC_p2_k256
c3_BMC_p2_k32
c3_BMC_p2_k4
c3_BMC_p2_k512
c3_BMC_p2_k64
c3_BMC_p2_k8
c4_BMC_p1_k1024
c4_BMC_p1_k128
c4_BMC_p1_k16
c4_BMC_p1_k2
c4_BMC_p1_k2048
c4_BMC_p1_k256
c4_BMC_p1_k32
c4_BMC_p1_k4
c4_BMC_p1_k512
c4_BMC_p1_k64
c4_BMC_p1_k8
c4_BMC_p2_k1024
c4_BMC_p2_k128
c4_BMC_p2_k16
c4_BMC_p2_k2
c4_BMC_p2_k2048
c4_BMC_p2_k256
c4_BMC_p2_k32
c4_BMC_p2_k4
c4_BMC_p2_k512
c4_BMC_p2_k64
c4_BMC_p2_k8
c5_BMC_p1_k1024
c5_BMC_p1_k128
c5_BMC_p1_k16
c5_BMC_p1_k2
c5_BMC_p1_k2048
c5_BMC_p1_k256
c5_BMC_p1_k32
c5_BMC_p1_k4
c5_BMC_p1_k512
c5_BMC_p1_k64
c5_BMC_p1_k8
c5_BMC_p2_k1024
c5_BMC_p2_k128
c5_BMC_p2_k16
c5_BMC_p2_k2
c5_BMC_p2_k2048
c5_BMC_p2_k256
c5_BMC_p2_k32
c5_BMC_p2_k4
c5_BMC_p2_k512
c5_BMC_p2_k64
c5_BMC_p2_k8
c6_BMC_p1_k1024
c6_BMC_p1_k128
c6_BMC_p1_k16
c6_BMC_p1_k2
c6_BMC_p1_k2048
c6_BMC_p1_k256
c6_BMC_p1_k32
c6_BMC_p1_k4
c6_BMC_p1_k512
c6_BMC_p1_k64
c6_BMC_p1_k8
c6_BMC_p2_k1024
c6_BMC_p2_k128
c6_BMC_p2_k16
c6_BMC_p2_k2
c6_BMC_p2_k2048
c6_BMC_p2_k256
c6_BMC_p2_k32
c6_BMC_p2_k4
c6_BMC_p2_k512
c6_BMC_p2_k64
c6_BMC_p2_k8
Contact
|
Organization
|
Links
|
Citing QBFLIB