The tool SMV2QBF is a bounded and unbounded model checker. It reads flat SMV models and generates propositional formulas or QBF as CNF in DIMACS format or And-Inverter-Graphs (AIGs) in AIGER format. The tool is the platform for the experiments described in our BMC'06 paper. QBF can only be dumped into (Q)DIMACS formats at the moment, e.g. AIGER is not supported yet. As model checking properties we only allow simple safety properties.


[ ]

We currently provide only some of the more interesting QBF instances used in the paper. The archive above also contains two scripts (one for SAT and one for UNSAT instances) to regenerate the examples.

[ smv2qbf-1.0.tar.gz ]

The archive contains the sources of our first public release. We use a BSD style LICENSE.