JKU

TNF / INF

team
contact
software
publications
teaching
jobs


GI-Dissertation Award 2020

FMCAD'20 Student Forum Best Student Contribution

SAT'20 Best Presentation Award

GCAI'19 Post and Interaction Award

IJCAI-JAIR 2019 Award

SAT'19 Best Student Paper

CAV'18 Award

HVC'17 Best Paper

ETAPS'17 Test of Time Award

HVC'15 Award

FMCAD'17 Best Paper

CADE'17 Best Paper

BMC

Handbook of Satisfiability

UML@Classroom

UML@Classroom

www.digitaltechnik.org

[  overview | download ]

SMV2QBF

Overview

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.

Download

[ JussilaBiere-BMC06-qbf-benchmarks.zip ]

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.