This tool includes both a Bounded Model Checker as well as an Interpolation-based Model Checker based on the material presented in class in the course Computer Aided Verification by Georg Weissenbacher at TU Wien and the description in [VWM2015].
It expects a transition system specified as an And-inverter graph in AIGER ASCII format with a single output interpreted as the bad property.
- -v Prints some interesting info while running the interpolation-based checker
- -V Prints more interesting info while running the interpolation-based checker
- -a n Limits inner loop iterations in the interpolation-based checker, i.e. the number of interpolants added to initial states
- -b n Limits outer loop iterations in the interpolation-based checker
To run the bounded model checking procedure simply pass a bound k before specifying the input file:
./modelchecker 42 input_file.aag
To run the interpolation-based checker simply specify an input file along with some optional parameters
./modelchecker input_file.aag
There is a Makefile attached. Adapt accordingly
For large instances one might run into a stack overflow, just increase the stack size if that is the case. At that point the solver is usually already struggling to come up with an answer.
On the sequential modelchecking benchmarks from 2006 provided on the AIGER FORMAT website, my tool performs comparable to nuXmv with a 5 minute timeout on my computer.