This page contains the source codes, benchmarks, and scripts for the experiments in the paper "Linear Encodings of Bounded LTL Model Checking" by Biere, Heljanko, Junttila, Latvala, and Schuppan, accepted to Logical Methods in Computer Science.

• The source code for liveness-to-safety translation by Viktor Schuppan is available here.
• The source code for the NuSMV version 2.2.3, augmented with the VMCAI 2005 BMC algorithm, by Timo Latvala is available here.
• The source code for the NuSMV version 2.2.3, augmented with the CAV 2005 BMC algorithm, by Tommi Junttila is available here.
• The benchmarks are available here.
• The scripts are available here.
• The result data and plots are available here.