CNF formulas generated with BMC

BMC-dimacs-examples-0.0.tar.gz

contains propositional formulas in conjunctive normal form (CNF), i.e. in DIMACS format, that have been generated by the bounded model checker BMC for three examples used in [1] and [2].

[1]

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic Model Checking without BDDs. In Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99), number 1579 in LNCS. Springer-Verlag, 1999.

[2]

A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic Model Checking using SAT procedures instead of BDDs. In Design Automation Conference (DAC'99), 1999.