Symbolic Model Checking of Product-Line Requirements Using SAT

Building the Tool

The instructions work on Ubuntu 14.04, minor modifications are required for Ubuntu 12.04.


Install the required packages:

sudo apt-get install -y gcc g++ mercurial make zlib1g-dev python-setuptools python-dev

Checking out the code

This repository uses Mercurial subrepositories to collect a few repositories with the code required to build this tool

hg clone

This will checkout all the relevant subrepositories

Building the code

Change into the newly created features_build directory and run the script


This will compile the code and build a gzipped tar with the distribution.


For the conversion script form SMV to AIGER examples to work, download NuSMV-2.5.0.tar.gz from and put in the parent directory of features_build. If the file is present, the build script will compile and build NuSMV, which is a requirement for the conversion script.

Building on Ubuntu 12.04

The only change requires is to modify the file features_build/pyzz/api/MODULE.conf. Replace -std=c++11 with -std=c++0x.