CAV05 submission source code

This page contains the source code and benchmarks for the NuSMV version used in the experiments of the paper "Incremental and Complete Bounded Model Checking for Full PLTL" by Heljanko, Junttila and Latvala, accepted to CAV 2005.

The source code is available here. This code replaces the "nusmv" directory in the NuSMV 2.2.3 distribution. That is, in order to compile the new system, download NuSMV 2.2.3 and zChaff, replace the nusmv directory, and compile as usual.
The new NuSMV version contains the following new commands.
- HJL_zigzag_inc_bmc
  The new translation with completeness check and incremental SAT solving.
- HJL_noninc_bmc
  The new translation with completeness check and non-incremental SAT solving.
- HJL_counterexample_inc_bmc
  The new translation without completeness check but with incremental SAT solving.
- HJL_counterexample_noninc_bmc
  The new translation without completeness check and with non-incremental SAT solving.
The benchmark files used in the paper:
- The VMCAI benchmark is available here
- The IBM benchmarks are from the paper "Simple yet efficient improvements of SAT based bounded model checking" by E. Zarpas, published in FMCAD 2004. Please ask the author of that paper for the benchmarks.
- The other benchmarks are part of the standard NuSMV 2.2.3 distribution, in the directory examples. "ctl-ltl/counter_1.smv" refers to the first LTLSPEC in the "ctl-ltl/counter.smv" file.