Experiments for VMCAI 2005

This pages contains the implementation and files related to the experiments performed in the paper:

Timo Latvala, Armin Biere, Keijo Heljanko and Tommi Junttila: Simple is Better: Efficient Bounded Model Checking for Past LTL, In R. Cousot (editor), Verification, Model Checking and Abstract Interpretation 2005, 5th International Conference VMCAI 2005, Paris, France. Volume 3385 of Lecture Notes in Computer Science, pp 380-395, Springer, 2005.

The modified version of NuSMV, version 2.1.2, we used is available here:

NuSMV-2.1.2.timo.tar.gz (2.6 MB).

The changes made to NuSMV are distributed under the conditions of the GNU LGPL., the same license as NuSMV. We are also distributing the scripts used perform the experiments to enable easy replication of our experiments. The scripts are distributed under the conditions of the GNU GPL. and are available here:

testscripts.tar.gz (10 KB).

models.tar.gz (95 KB).

These can be used with the testscripts above The real-life models with their specfication can be found here:

realmodels.tar.gz (10 KB).