Getafix: A symbolic model-checker for recursive programs

Experiments on sequential benchmarks:

Experiments on an extensive set of benchmarks are given below. The benchmarks are:

Regression suite for SLAM

Driver programs from SLAM benchmarks (Driver and iscsi)

Three benchmark examples from Terminator.

In all experiments, Getafix is pretty much as fast as model-checkers Moped and Bebop. And on the more complex Terminator benchmarks, Getafix performs way better than Moped and Bebop (in one example, Getafix terminates in 12s while the others don't even finish in 30 minutes).

									Getafix			Moped Ver#1	Moped Ver#2	Bebop
	#LOC	#ret	#param.	#globals (g)	#locals	max locals per proc. (l)	# proce- dures	Reach?	Peak #Nodes in BDD	Time(s)		Time(s)	Time(s)	Time(s)
										EF	EF opt
Regression
Positive (99 programs)	368	1.8	2.3	0.8	4.8	3.2	6.9	Yes	240	1	1	1	1	1
Negative (79 programs)	224	1.9	2.5	2	8.2	3.6	6.5	No	625	1	1	1	1	1
Slam
Driver iscsiprt (positive) (15 programs)	10K	10	9	3.5	211	11.8	148	Yes	8K	2	2	1	1	1
Driver floppy (positive) (12 programs)	17K	15	12	5.3	172.5	16	103	Yes	9K	2	2	1	1	1
Driver (negative) (4 programs)	10K	11	8.25	10.7	154.2	12	116.2	No	17K	2	2	1	1	1
iscsi (positive) (16 programs)	12K	18	18	17.1	358.8	18	158	Yes	81K	5	5	2	4	6
Terminator
Terminator-A (iterative)	284	18	12	9	97	68	4	Yes	141K	4	3	-	1	4
Terminator-A (schoose)	284	18	12	9	97	68	4	Yes	162K	3	3	14	1	3
Terminator-B (iterative)	471	9	7	14	77	42	4	No	997K	72	12	-	-	-
Terminator-B (schoose)	471	9	7	14	77	42	4	No	660K	32	9	24	490	953
Terminator-C (iterative)	908	1	0	23	19	19	4	No	48K	2	3	1	1	711
Terminator-C (schoose)	908	1	0	23	19	19	4	No	48K	2	3	1	1	709

Legend:
  "LOC denotes the average number of lines of code for each set of programs.
  "-" denotes timeout in 30 minutes.
  #Nodes in BDD reported is the peak BDD size of the set of summaries computed by Getafix;
    --- note that this is the same for both the EF and EF-opt versions.