This repository contains the assignments for the course "Software Model Checking" at TU Vienna. These assignments are programming exercises, meaning that working code solutions have to be handed in by the participants.
The code in this repository can be used as a template for the solution, but participants are free to develop their solutions in any programming language or framework they choose, provided that
- The project can be built using publically available tools and compilers.
- The project can be run on a linux machine.
The following software is required to build the framework:
- CMake is used as a build tool. At least version 2.6 is required. Most distributions provide binary packages.
- MathSAT is used as the SMT solver backend. Binary packages for Linux, MacOS and Windows are available.
To build the framework, first create a build directory
mkdir build cd build
then generate Makefiles using
cmake ..
and finally compile the project
make
If everything worked out, you should end up with a executable "smc" in the build directory. It can be executed in bounded-model-checking (BMC) mode using
./smc bmc 10 < ../tests/sum.l
or in predicate abstraction mode using
./smc pred_abs < ../tests/sum.l