The RocketScience state-of-the-art model checker for sequential recursive recursive integer programs was developed during a masters project in the Concurrency Theory Group at the University of Kaiserslautern during a masters project.
It is implemented in C++ and integrates the following techniques:
- CEGAR loop
- Predicate Abstraction
- Procedure Summaries
- Reachability Analysis
- Refinement based on Craig Interpolants
- Boost >= 1.57 (C++11 support)
- CMake >= 3.1.0
- Z3 >= 4.3.2 (with C++ bindings)
make the project. The result can be found in the
Tested on Mac OS X Yosemite 10.10.3 with Command Line Tools 6.2.
After making the project, you can simply call
RocketScience with a file containing a program. You can run a simple test via
make test or specify your own program like so: