This page provides experimental results of running Blast on several sets of benchmark programs. The numbers on this page were generated by running Blast on a 3.6GHz Linux machine  with 1GB of RAM. These results can be reproduced by running the regression test script regrtest in blast/test in the Blast distribution. The regrtest script provides more numbers such as the number of iterations for reachability, the size of the reachable state space, and the number of predicates.

Windows Driver Experiments

SSH Experiments

ssh is the implementation of the SSH protocol. The following files were provided by Sagar Chaki and already instrumented with the properties. All the properties are safe.
You can generate these results by running
       ./regrtest -block CHAKI -perf
in the blast/test directory.

Instrumented File
Blast command line
Time
[0] s3_clnt.blast.1.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_clnt.blast.1.c  0.850s
[1] s3_clnt.blast.2.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_clnt.blast.2.c  0.856s
[2] s3_clnt.blast.3.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_clnt.blast.3.c 0.854s
[3] s3_clnt.blast.4.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_clnt.blast.4.c 0.860s
[4] s3_srvr.blast.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.c 0.684s
[5] s3_srvr.blast.1.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.1.c 0.718s
[6] s3_srvr.blast.2.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.2.c 0.711s
[7] s3_srvr.blast.3.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.3.c 0.704s
[8] s3_srvr.blast.4.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.4.c 0.704s
[9] s3_srvr.blast.5.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.5.c 0.757s
[10] s3_srvr.blast.6.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.6.c 0.699s
[11] s3_srvr.blast.7.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.7.c 0.755s
[12] s3_srvr.blast.8.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.8.c 0.657s
[13] s3_srvr.blast.9.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.9.c 0.751s
[14] s3_srvr.blast.10.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.10.c 0.645s
[15] s3_srvr.blast.11.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.11.c 0.752s
[16] s3_srvr.blast.12.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.12.c 0.665s
[17] s3_srvr.blast.13.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.13.c 0.751s
[18] s3_srvr.blast.14.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.14.c 0.671s
[19] s3_srvr.blast.15.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.15.c 0.664s
[20] s3_srvr.blast.16.c
time ../bin/pblast.opt -nofp -predH 7 ssh/s3_srvr.blast.16.c 0.684s




TCAS Experiments

TCAS is an implementation of a traffic collision avoidance system provided to us by Himanshu Jain. The program was already instrumented with the properties. You can generate these results by running
          ./regrtest -block TCAS -perf
in the blast/test directory.

Property
Blast Command Line
Safe/Unsafe
Time taken
PROPERTY1A
time ../bin/pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY1A
SAFE
2.029s
PROPERTY1B
time ../bin/pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY1B SAFE
19.793s
PROPERTY2A
time ../bin/pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY2A SAFE
2.111s
PROPERTY3B
time ../bin/pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY3B SAFE
5.235s
PROPERTY2B
time ../bin/pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY2B UNSAFE
8.452s
PROPERTY5A
time ../bin/pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY5A SAFE
3.118s
PROPERTY3A
time ../bin/pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY3A UNSAFE
2.868s
PROPERTY4A
time ../bin/pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY4A UNSAFE
6.795s
PROPERTY4B
time ../bin/pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY4B UNSAFE
7.088s
PROPERTY5B
time ../bin/pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY5B UNSAFE
10.683s