Symbolic Model Checking of Product-Line Requirements Using SAT

Running the Tool

Run the script in the bin subdirectory

features_distribution/bin/ [options] ....

Try the --help flag to see the available options.

How to convert SMV benchmarks

The archive contains a script to convert SMV benchmarks to AIGER files that can be run by our tool:

features_distribution/bin/ file.smv

This script uses NuSMV 2.5.0, as our tools use the AIGER format natively.