TCS / ~timo/ vmcai2005/
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

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).

The random models and formulas used to generate the data for the picutures in the paper are also available:

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).

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 01 December 2004.