Reducer-Based Construction of Conditional Verifiers -- Full Version of Table 3

Full Version of Table 3 in the Paper

The following table shows a subset of the hard verification tasks of the verifiers. It contains all 144 tasks that none of the verifiers CPAseq, Smack, and Ultimate Automizer can solve as standard verifier but at least one reducer-based combination can. Column R shows the expected result of the corresponding task: either no property violation exists (T) in the program or a property violation exists (F). Column S reports whether the task was solved by the corresponding verifier, t is the CPU time in seconds spent to achieve the corresponding result, and M the used memory in GB.


Task	R	CPAseq			SMACK			UAutomizer			+CPAseq			+SMACK			+UAutomizer
		S	t(s)	M(GB)	S	t(s)	M(GB)	S	t(s)	M(GB)	S	t(s)	M(GB)	S	t(s)	M(GB)	S	t(s)	M(GB)

loop-acc overflow	T	✘	910	7.8	✘	880	0.93	✘	900	1.3	✔	2.6	0.27	✔	2.6	0.27	✔	2.6	0.27
mutex_unbounded	F	✘	910	4.9	✘	0.13	0.021	✘	900	0.94	✔	5.6	0.32	✔	5.6	0.32	✔	5.6	0.32
mutex_unlock	F	✘	320	4.9	✘	0.11	0.020	✘	900	1.2	✔	11	0.47	✔	11	0.47	✔	11	0.47
lin-4.0 legousbtower	F	✘	180	15	✘	880	0.56	✘	900	4.0	✔	12	0.48	✔	12	0.48	✔	12	0.48
lin-4.0 net2272	F	✘	56	15	✘	890	1.0	✘	900	7.3	✔	15	0.53	✔	15	0.53	✔	15	0.53
fib_longer	F	✘	900	3.7	✘	880	0.15	✘	8.6	0.30	✔	15	0.61	✔	15	0.61	✔	15	0.61
lin-3.4 vivi	F	✘	230	15	✘	880	0.25	✘	48	1.3	✔	15	0.59	✔	15	0.59	✔	15	0.59
lin-3.0 block-loop	F	✘	900	8.5	✘	880	0.48	✘	900	3.8	✔	16	0.51	✔	16	0.51	✔	16	0.51
lin-4.2 lm78	T	✘	950	6.8	✘	890	1.2	✘	910	13	✔	18	0.63	✔	18	0.63	✔	18	0.63
lin-3.4 synaptics	F	✘	210	15	✘	880	0.43	✘	900	1.6	✔	18	0.62	✔	18	0.62	✔	18	0.62
lin-3.16 mISDN	T	✘	910	8.8	✘	950	3.0	✘	900	5.7	✔	26	0.96	✔	26	0.96	✔	26	0.96
lin-4.2 vfio	F	✘	910	8.1	✘	890	0.47	✘	900	5.3	✔	26	0.70	✔	26	0.70	✔	26	0.70
val-0.8 g_printer	F	✘	910	8.4	✘	880	0.73	✘	900	5.5	✔	28	0.87	✔	28	0.87	✔	28	0.87
val-06 g_printer	F	✘	910	8.4	✘	880	0.71	✘	900	5.6	✔	28	0.85	✔	28	0.85	✔	28	0.85
lin-3.14 alloc-fealnx	T	✘	910	7.7	✘	190	14	✘	900	6.7	✔	29	1.0	✔	29	1.0	✔	29	1.0
lin-4.0 broadcom--tg3	F	✘	190	15	✘	950	8.4	✘	25	0.62	✔	29	0.93	✔	29	0.93	✔	29	0.93
lin-4.0 ubi	F	✘	940	9.8	✘	270	14	✘	22	0.56	✔	33	1.1	✔	33	1.1	✔	33	1.1
li-3.14 alloc-pcnet32	T	✘	920	7.7	✘	910	5.3	✘	900	13	✔	34	1.1	✔	34	1.1	✔	34	1.1
lin-4.0 ide--ide	F	✘	960	11	✘	920	1.5	✘	900	5.6	✔	34	1.1	✔	34	1.1	✔	34	1.1
fib	F	✘	910	4.5	✘	880	0.16	✘	8.7	0.31	✔	34	1.2	✔	34	1.2	✔	34	1.2
lin-3.8 32_7a vmwgfx	F	✘	320	15	✘	910	1.6	✘	20	0.49	✔	35	1.1	✔	35	1.1	✔	35	1.1
lin-4.2 lloop	F	✘	950	8.6	✘	880	0.29	✘	900	1.0	✔	36	1.2	✔	36	1.2	✔	36	1.2
1dfa93a-kobil	F	✘	210	15	✘	880	0.33	✘	11	0.34	✔	37	1.2	✔	37	1.2	✔	37	1.2
lin-3.16 usb8xxx	F	✘	950	5.3	✘	880	0.35	✘	900	3.5	✔	43	1.2	✔	43	1.2	✔	43	1.2
lin-4.0 8390--pcnet	F	✘	920	7.4	✘	910	4.0	✘	900	9.4	✔	47	1.7	✔	47	1.7	✔	47	1.7
lin-4.0 wdm	F	✘	350	15	✘	880	0.37	✘	900	5.5	✔	50	1.2	✔	50	1.2	✔	50	1.2
lin-4.0 usbtouchscreen	F	✘	850	15	✘	880	0.57	✘	900	7.0	✔	51	1.5	✔	51	1.5	✔	51	1.5
lin-4.0 mtip32xx	F	✘	930	15	✘	890	3.7	✘	900	11	✔	52	1.4	✔	52	1.4	✔	52	1.4
lin-4.0 atm--fore	F	✘	430	15	✘	890	1.2	✘	14	0.43	✔	54	1.6	✔	54	1.6	✔	54	1.6
lin-3.0 keyspan	F	✘	950	5.2	✘	880	0.85	✘	900	2.8	✔	56	2.1	✔	56	2.1	✔	56	2.1
cs_queue	F	✘	900	6.8	✘	880	0.63	✘	52	8.3	✔	58	2.1	✔	58	2.1	✔	58	2.1
lin-4.0 netxen	F	✘	960	11	✘	940	2.4	✘	19	0.50	✔	64	2.3	✔	64	2.3	✔	64	2.3
lin-3.16 lapbether	T	✘	910	10	✘	880	0.30	✘	110	1.3	✔	64	2.5	✔	64	2.5	✔	64	2.5
lin-4.2 block-loop	F	✘	910	7.9	✘	880	0.54	✘	910	13	✔	66	2.4	✔	66	2.4	✔	66	2.4
lin-3.16 can-dev	T	✘	910	7.2	✘	880	0.95	✘	900	11	✔	66	2.0	✔	66	2.0	✔	66	2.0
pipeline	T	✘	920	4.4	✘	880	0.67	✘	910	13	✔	73	2.7	✔	73	2.7	✔	73	2.7
lin-4.2 hwmon-it87	T	✘	920	5.9	✘	900	6.0	✘	910	13	✔	80	3.1	✔	80	3.1	✔	80	3.1
lin-4.2 hwmon-w83627hf	T	✘	920	7.6	✘	900	4.6	✘	900	14	✔	87	2.9	✔	87	2.9	✔	87	2.9
lin-4.2 solos-pci	T	✘	910	7.8	✘	890	2.7	✘	910	14	✔	92	2.1	✔	92	2.1	✔	92	2.1
lin-3.14 complex-can-mcp251x	T	✘	950	7.8	✘	880	0.65	✘	900	13	✔	100	3.9	✔	100	3.9	✔	100	3.9
lin-4.2 io_edgeport	T	✘	910	7.6	✘	880	1.5	✘	900	14	✔	100	3.6	✔	100	3.6	✔	100	3.6
lin-4.2 32_7a-b43	T	✘	920	14	✘	950	0.88	✘	20	0.51	✔	100	3.8	✔	100	3.8	✔	100	3.8
image_filter	T	✘	240	15	✘	60	15	✘	5.0	0.30	✔	100	3.1	✔	100	3.1	✔	100	3.1
Problem17_label47	T	✘	910	14	✘	880	3.1	✘	900	2.5	✔	110	0.25	✘	110	0.25	✔	110	0.32
Problem17_label48	T	✘	850	15	✘	880	3.0	✘	900	0.72	✔	110	0.25	✘	110	0.25	✔	110	0.31
Problem17_label59	T	✘	910	9.9	✘	880	3.0	✘	900	6.3	✔	110	0.25	✘	110	0.24	✔	110	0.32
filter2_iterated	T	✘	9.0	0.74	✘	39	15	✘	38	2.2	✔	110	0.27	✘	100	0.25	✘	150	2.2
Problem13_label18	T	✘	520	15	✘	880	3.1	✘	900	8.5	✔	110	0.29	✘	110	0.29	✔	110	0.35
Problem13_label08	T	✘	510	15	✘	880	3.1	✘	910	11	✔	110	0.30	✘	110	0.29	✔	110	0.32
Problem19_label54	T	✘	450	15	✘	880	2.9	✘	900	13	✔	110	0.38	✘	110	0.37	✔	110	0.38
Problem19_label02	T	✘	450	15	✘	880	2.9	✘	900	11	✔	110	0.37	✘	110	0.37	✔	110	0.38
Problem19_label08	T	✘	440	15	✘	880	3.0	✘	910	12	✔	110	0.37	✘	110	0.39	✔	110	0.37
Problem19_label35	T	✘	440	15	✘	880	2.9	✘	910	14	✔	110	0.36	✘	110	0.37	✔	110	0.37
Problem19_label38	T	✘	440	15	✘	880	3.0	✘	900	7.0	✔	110	0.37	✘	110	0.37	✔	110	0.37
Problem13_label01	T	✘	490	15	✘	880	3.1	✘	900	8.9	✔	110	0.28	✘	110	0.29	✔	110	0.32
Problem19_label23	T	✘	450	15	✘	880	2.9	✘	910	13	✔	110	0.36	✘	110	0.37	✔	110	0.38
Problem19_label45	T	✘	460	15	✘	880	2.8	✘	900	11	✔	110	0.37	✘	110	0.38	✔	110	0.39
Problem19_label48	T	✘	500	15	✘	880	2.9	✘	900	13	✔	110	0.37	✘	110	0.37	✔	110	0.37
Problem19_label24	T	✘	440	15	✘	880	2.9	✘	900	12	✔	110	0.37	✘	110	0.36	✔	120	0.38
Problem19_label46	T	✘	450	15	✘	880	2.9	✘	910	11	✔	110	0.37	✘	110	0.37	✔	110	0.38
Problem19_label20	T	✘	520	15	✘	880	2.8	✘	900	13	✔	110	0.37	✘	110	0.37	✔	110	0.37
Problem19_label57	T	✘	440	15	✘	880	2.9	✘	900	13	✔	110	0.36	✘	110	0.37	✔	110	0.38
Problem19_label37	T	✘	440	15	✘	880	3.2	✘	900	13	✔	110	0.38	✘	110	0.37	✔	110	0.37
Problem19_label15	T	✘	440	15	✘	880	3.0	✘	900	11	✔	110	0.37	✘	110	0.37	✔	110	0.38
Problem19_label44	T	✘	440	15	✘	880	2.9	✘	900	12	✔	110	0.39	✘	110	0.37	✔	110	0.37
Problem19_label36	T	✘	500	15	✘	880	2.9	✘	900	13	✔	110	0.38	✘	110	0.38	✔	120	0.38
Problem19_label06	T	✘	460	15	✘	880	2.9	✘	910	14	✔	110	0.37	✘	110	0.38	✔	110	0.36
Problem19_label56	T	✘	440	15	✘	880	2.9	✘	910	13	✔	110	0.39	✘	110	0.37	✔	110	0.37
Problem19_label30	T	✘	450	15	✘	880	3.2	✘	910	13	✔	110	0.36	✘	110	0.37	✔	110	0.37
Problem19_label01	T	✘	440	15	✘	880	2.9	✘	900	11	✔	110	0.37	✘	110	0.37	✔	110	0.37
Problem19_label09	T	✘	550	15	✘	880	3.0	✘	900	11	✔	110	0.37	✘	110	0.37	✔	110	0.37
Problem19_label40	T	✘	450	15	✘	880	2.9	✘	900	13	✔	110	0.38	✘	110	0.37	✔	110	0.36
Problem13_label33	T	✘	550	15	✘	880	3.1	✘	900	7.2	✔	110	0.29	✘	110	0.30	✔	110	0.32
Problem19_label05	T	✘	450	15	✘	880	2.9	✘	900	12	✔	110	0.38	✘	110	0.37	✔	110	0.36
Problem19_label52	T	✘	450	15	✘	880	2.9	✘	900	12	✔	110	0.37	✘	110	0.37	✔	120	0.37
Problem19_label33	T	✘	500	15	✘	880	3.2	✘	900	6.7	✔	110	0.37	✘	110	0.38	✔	110	0.39
Problem19_label12	T	✘	440	15	✘	880	2.9	✘	900	13	✔	110	0.36	✘	110	0.37	✔	110	0.36
Problem19_label34	T	✘	460	15	✘	880	2.9	✘	910	12	✔	110	0.36	✘	110	0.37	✔	110	0.37
Problem19_label39	T	✘	490	15	✘	880	2.8	✘	900	13	✔	110	0.37	✘	110	0.38	✔	110	0.37
Problem19_label16	T	✘	460	15	✘	880	3.0	✘	900	13	✔	110	0.37	✘	110	0.36	✔	110	0.37
Problem19_label00	T	✘	500	15	✘	880	3.5	✘	900	14	✔	110	0.37	✘	110	0.36	✔	110	0.37
Problem13_label03	T	✘	510	15	✘	880	3.1	✘	900	6.4	✔	110	0.28	✘	110	0.29	✔	110	0.32
Problem19_label49	T	✘	440	15	✘	880	2.9	✘	910	13	✔	110	0.37	✘	110	0.37	✔	110	0.37
Problem19_label07	T	✘	500	15	✘	880	2.9	✘	900	12	✔	110	0.37	✘	110	0.37	✔	110	0.38
Problem19_label25	T	✘	530	15	✘	880	2.9	✘	910	13	✔	110	0.39	✘	110	0.38	✔	110	0.38
Problem19_label03	T	✘	450	15	✘	880	2.9	✘	900	13	✔	110	0.37	✘	110	0.37	✔	120	0.37
Problem13_label38	T	✘	520	15	✘	880	3.1	✘	900	8.2	✔	110	0.31	✘	110	0.29	✔	110	0.32
Problem13_label39	T	✘	480	15	✘	880	3.1	✘	900	11	✔	110	0.29	✘	110	0.28	✔	110	0.32
Problem19_label04	T	✘	530	15	✘	880	2.9	✘	900	11	✔	110	0.38	✘	110	0.37	✔	110	0.36
Problem19_label13	T	✘	530	15	✘	880	2.9	✘	900	12	✔	110	0.37	✘	110	0.36	✔	110	0.36
Problem13_label42	T	✘	510	15	✘	880	3.3	✘	910	10	✔	110	0.31	✘	110	0.31	✔	120	0.32
Problem13_label49	T	✘	530	15	✘	880	3.1	✘	900	9.1	✔	110	0.30	✘	110	0.29	✔	120	0.35
Problem13_label34	T	✘	560	15	✘	880	3.1	✘	900	7.4	✔	110	0.29	✘	110	0.30	✔	120	0.32
lin-3.16 arc-rawmode	T	✘	950	4.4	✘	880	0.50	✘	900	0.99	✔	110	0.44	✘	110	0.43	✘	110	0.44
Problem15_label01	T	✘	910	10	✘	880	1.9	✘	900	3.1	✔	120	0.55	✘	110	0.55	✔	130	0.62
Problem17_label51	T	✘	770	15	✘	880	3.1	✘	900	7.9	✔	120	0.58	✘	110	0.59	✘	130	0.58
Problem17_label36	T	✘	910	14	✘	880	3.0	✘	900	0.65	✔	120	0.58	✘	110	0.57	✘	130	0.57
Problem17_label29	T	✘	910	14	✘	880	3.0	✘	900	3.6	✔	120	0.57	✘	110	0.59	✘	130	0.60
Problem17_label05	T	✘	910	14	✘	880	3.1	✘	900	3.7	✔	120	0.58	✘	110	0.58	✘	130	0.58
Problem17_label14	T	✘	910	14	✘	880	3.0	✘	900	4.2	✔	120	0.58	✘	110	0.58	✘	130	0.59
Problem17_label22	T	✘	910	15	✘	880	3.1	✘	900	6.2	✔	120	0.58	✘	110	0.58	✘	130	0.60
Problem17_label19	T	✘	850	15	✘	880	3.1	✘	900	6.6	✔	120	0.57	✘	110	0.58	✘	130	0.58
Problem17_label15	T	✘	910	15	✘	880	3.0	✘	900	4.3	✔	120	0.57	✘	110	0.57	✘	130	0.57
Problem17_label03	T	✘	910	14	✘	880	3.1	✘	900	1.9	✔	120	0.57	✘	110	0.58	✘	130	0.58
Problem17_label43	T	✘	780	15	✘	880	2.9	✘	900	6.1	✔	120	0.57	✘	110	0.58	✘	130	0.59
Problem17_label17	T	✘	910	14	✘	880	2.9	✘	900	3.0	✔	120	0.57	✘	110	0.58	✘	130	0.57
Problem17_label56	T	✘	890	15	✘	880	3.0	✘	900	0.69	✔	120	0.58	✘	110	0.58	✔	170	0.88
Problem17_label06	T	✘	910	14	✘	880	3.1	✘	900	3.8	✔	120	0.60	✘	110	0.58	✘	130	0.58
Problem17_label44	T	✘	910	15	✘	880	3.2	✘	900	0.82	✔	120	0.57	✘	110	0.58	✔	140	0.85
Problem17_label38	T	✘	840	15	✘	880	3.1	✘	900	5.0	✔	120	0.58	✘	120	0.59	✘	130	0.57
Problem07_label56	T	✘	950	6.8	✘	530	15	✘	910	13	✔	130	0.93	✘	130	0.93	✔	130	0.93
lin-3.16 pvrusb2	T	✘	950	7.2	✘	930	3.2	✘	8.3	0.40	✔	160	0.88	✘	150	0.87	✔	160	0.86
lin-4.2 pvrusb2	T	✘	960	11	✘	930	3.3	✘	9.6	0.43	✔	160	0.88	✘	150	0.89	✔	160	0.90
lin-4.2 speakup	T	✘	920	6.8	✘	910	7.3	✘	10	0.52	✔	180	0.94	✘	180	0.93	✔	180	0.93
mutex_double_unlock	F	✘	950	11	✘	0.12	0.021	✘	900	1.3	✘	940	2.4	✘	100	0.25	✔	230	1.0
newton_3_6	F	✘	950	5.0	✘	890	1.3	✘	490	15	✘	910	3.1	✘	6.2	0.22	✔	260	10
lin-3.14 locking-mutex-mxl111sf	T	✘	910	5.8	✘	890	0.71	✘	910	14	✘	260	1.5	✘	260	1.5	✔	270	1.5
lin-3.14 locking-spinlock-vsp1	T	✘	920	7.1	✘	890	0.78	✘	910	12	✘	300	1.5	✘	300	1.4	✔	300	1.5
lin-4.2 packetengines-hamachi	T	✘	940	7.5	✘	110	14	✘	900	14	✔	310	8.0	✘	120	0.62	✘	140	0.93
Problem07_label02	T	✘	950	6.8	✘	900	14	✘	900	13	✘	460	1.4	✘	450	1.4	✔	340	1.4
Problem07_label14	T	✘	950	6.8	✘	500	15	✘	910	12	✘	1100	1.4	✘	320	1.4	✔	350	1.4
Problem07_label55	T	✘	950	6.9	✘	230	7.5	✘	910	11	✘	490	1.4	✘	1100	1.4	✔	350	1.4
lin-3.14 locking-mutex-bt8xx	T	✘	950	6.2	✘	910	5.1	✘	20	0.55	✘	360	1.5	✘	410	1.5	✔	370	1.5
lin-4.2 icplus	T	✘	950	8.0	✘	910	5.5	✘	900	13	✔	380	10	✘	120	0.60	✘	140	1.1
Problem07_label01	T	✘	950	6.8	✘	230	7.2	✘	900	13	✘	440	1.4	✘	330	1.4	✔	420	1.4
Problem07_label34	T	✘	950	7.1	✘	250	7.2	✘	900	12	✘	340	1.5	✘	1100	1.4	✔	420	1.4
lin-3.14 hostap	T	✘	950	7.3	✘	910	1.3	✘	15	0.40	✘	390	1.5	✘	410	1.5	✔	420	1.5
Problem07_label26	T	✘	950	6.9	✘	230	7.2	✘	900	12	✘	340	1.4	✘	1100	1.4	✔	450	1.4
floodmax.4	T	✘	910	2.5	✘	880	0.53	✘	910	13	✔	450	2.9	✘	110	0.43	✘	1100	7.4
Problem07_label52	T	✘	950	7.1	✘	240	7.2	✘	900	12	✘	450	1.4	✘	460	1.4	✔	470	1.4
Problem07_label38	T	✘	950	7.5	✘	230	7.5	✘	910	12	✘	1100	1.4	✘	1100	1.4	✔	470	1.4
lin-4.2 vlsi_ir	T	✘	910	7.9	✘	890	0.97	✘	900	13	✔	490	10	✘	130	0.67	✘	150	0.77
lin-3.14 vsp1	T	✘	920	6.9	✘	890	0.70	✘	910	14	✘	550	1.5	✘	610	1.5	✔	640	1.5
lin-3.14 vxge	T	✘	930	11	✘	190	14	✘	19	0.51	✘	760	1.4	✘	630	1.5	✔	650	1.5
lin-4.2 w83781d	T	✘	910	6.7	✘	900	3.7	✘	910	14	✘	690	1.5	✘	660	1.4	✔	660	1.5
lin-4.2 zd1211rw	T	✘	930	6.3	✘	890	0.96	✘	140	11	✘	720	1.5	✘	670	1.5	✔	660	1.5
lin-3.14 vmxnet3	T	✘	930	6.9	✘	890	1.2	✘	900	10	✘	540	1.5	✘	640	1.4	✔	670	1.4
lin-3.14 skge	T	✘	950	7.3	✘	940	3.6	✘	410	15	✘	650	1.5	✘	600	1.5	✔	670	1.5
lin-3.16 ath5k	T	✘	950	5.9	✘	950	4.7	✘	900	13	✘	710	1.5	✘	730	1.5	✔	710	1.5
lin-3.14 ipw2200	T	✘	950	7.6	✘	950	6.6	✘	15	0.39	✘	700	1.5	✘	730	1.5	✔	720	1.5
lin-3.14 bttv	T	✘	950	5.8	✘	910	5.0	✘	20	0.51	✘	720	1.5	✘	770	1.4	✔	750	1.5
lin-4.2 cciss	T	✘	920	7.1	✘	330	12	✘	900	4.7	✔	790	10	✘	120	0.77	✘	180	5.3
opt-floodmax.4	T	✘	910	3.0	✘	880	0.53	✘	910	13	✔	900	4.3	✘	110	0.42	✘	1100	7.9
sep20	T	✘	900	3.2	✘	880	0.10	✘	910	13	✔	1000	2.6	✘	110	0.27	✘	150	0.99

Sum		0	100k	1600	0	120k	500	0	110k	1200	121	28k	180	43	24k	130	122	25k	170
Average			720	11		800	3.5		760	8.0		200	1.3		170	0.91		170	1.1