CSI

This site provides experiments for the paper CSI: New Evidence – A Progress Report by Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp.

Experiments for Confluence of TRSs (Table 1)

For experiments we considered the 291 TRSs in Cops. We compared the power of the current version of CSI (1.0) to its initial release (CSI 0.1) and to the version used in CoCo 2016 (0.6). The fourth column shows the results when using CSI's certifiable strategy, i.e., only criteria that can be checked by CETA, whose verdict is shown in the fifth column. Note that clicking a cell in the Results table below shows the corresponding tool output.

Statistics

	CSI-0.1	CSI-0.6	CSI-1.0	✔CSI-1.0	CeTA
#yes	115	179	206	116	177
total time	130.2	212.6	308.5	46.3	13.4
average time	1.1	1.2	1.5	0.4	0.1
#no	46	55	61	61	0
total time	12.5	33.9	112.9	69.7	0.0
average time	0.3	0.6	1.9	1.1	-
#maybe	111	15	14	31	0
total time	652.9	221.6	209.4	609.3	0.0
average time	5.9	14.8	15.0	19.7	-
#timeout	18	30	9	53	0
total time	1080.0	1800.0	540.0	3180.0	0.0
average time	60.0	60.0	60.0	60.0	-
#error	1	12	1	30	0
total time	0.6	394.3	34.7	968.5	0.0
average time	0.6	32.9	34.7	32.3	-
#total	291	291	291	291	177
total time	1876.2	2662.3	1205.5	4873.8	13.4

Results

	CSI-0.1	CSI-0.6	CSI-1.0	✔CSI-1.0	CeTA
1	0.3	0.5	0.8	0.3	0.0
2	0.2	0.4	0.7	60.0
3	0.2	0.4	0.7	18.3
4	0.2	0.5	0.8	0.2	0.0
5	0.1	0.3	0.4	0.2	0.0
6	0.1	0.3	0.4	0.2	0.0
7	0.1	0.3	0.4	0.2	0.0
8	0.2	0.7	1.1	0.3	0.0
9	0.1	0.4	0.4	0.2	0.0
10	0.1	0.4	0.4	0.2	0.0
11	0.2	0.5	0.6	0.2	0.0
12	0.1	0.3	0.4	0.2	0.0
13	0.1	0.3	0.4	0.2	0.0
14	0.1	0.5	0.6	0.2	0.0
15	60.0	60.0	10.4	6.2	0.0
16	1.2	14.5	1.5	1.5	0.0
17	6.2	0.5	0.6	21.6
18	0.2	0.4	0.5	0.2	0.0
19	0.2	0.5	0.5	0.3	0.0
20	0.9	0.8	1.0	0.3	0.0
21	0.1	0.5	0.7	0.3	0.0
22	1.3	0.7	0.8	0.3	0.0
23	0.1	0.4	0.5	0.2	0.0
24	6.1	60.0	20.5	12.3	0.1
25	6.1	2.1	2.5	60.0
	CSI-0.1	CSI-0.6	CSI-1.0	✔CSI-1.0	CeTA
26	6.1	60.0	60.0	60.0
27	1.2	15.5	15.8	18.4
28	6.1	1.7	1.9	60.0
29	0.1	0.3	0.5	0.3	0.0
30	1.7	0.6	1.0	0.3	0.0
31	0.1	0.3	0.4	0.2	0.0
32	0.1	0.4	0.4	0.2	0.0
33	1.2	0.6	0.7	0.3	0.0
34	1.2	0.3	0.5	0.3	0.0
35	0.1	0.4	0.7	0.2	0.0
36	1.2	0.4	0.6	0.2	0.3
37	1.2	0.6	0.8	0.3	0.0
38	0.2	0.5	0.6	0.3	0.0
39	0.1	0.5	0.6	0.2	0.0
40	0.1	0.4	0.5	0.3	0.0
41	0.1	0.4	0.6	0.2	0.0
42	0.4	0.8	0.9	0.4	0.0
43	0.1	0.4	0.4	0.2	0.0
44	0.1	0.3	0.4	0.2	0.0
45	0.1	0.5	0.6	0.2	0.0
46	0.1	0.4	0.5	0.2	0.0
47	6.1	60.0	14.2	10.1	0.0
48	2.4	0.7	0.8	0.3	0.0
49	0.1	0.8	0.8	1.5	0.0
50	0.2	0.6	0.6	0.3	0.0
	CSI-0.1	CSI-0.6	CSI-1.0	✔CSI-1.0	CeTA
51	0.3	0.4	0.5	0.3	0.0
52	2.0	14.7	14.8	14.8
53	0.2	0.4	0.7	20.7
54	1.3	14.5	14.8	12.1
55	0.3	0.4	0.6	14.0
56	1.2	14.6	14.8	12.7
57	1.2	14.6	14.8	9.1
58	1.9	14.7	14.9	14.8
59	1.1	0.3	0.5	18.3
60	3.7	5.7	5.9	0.8	0.3
61	6.1	0.5	1.0	0.3	0.0
62	6.1	0.6	0.8	60.0
63	1.4	0.4	0.8	0.3	0.0
64	0.1	0.7	0.8	1.5	0.0
65	0.3	0.4	0.9	0.3	0.0
66	0.2	0.5	0.6	0.3	0.0
67	0.2	0.4	0.5	0.3	0.0
68	0.2	0.6	0.7	0.3	0.0
69	0.2	0.5	0.7	0.2	0.0
70	0.1	0.3	0.5	0.2	0.0
71	0.2	0.5	0.8	0.2	0.0
72	0.2	0.5	0.5	0.2	0.0
73	0.2	0.4	0.5	0.3	0.0
74	1.3	0.5	0.8	0.2	0.0
75	1.1	0.5	0.5	0.3	0.0
	CSI-0.1	CSI-0.6	CSI-1.0	✔CSI-1.0	CeTA
76	60.0	60.0	0.6	60.0
77	60.0	60.0	3.3	60.0
78	60.0	60.0	11.8	7.5	0.0
79	6.1	0.4	0.4	60.0
80	0.1	0.4	0.6	0.2	0.0
81	1.2	0.6	0.7	0.3	0.0
82	0.1	0.5	0.7	0.2	0.0
83	0.2	0.5	0.6	0.3	0.0
84	0.1	0.4	0.5	0.3	0.0
85	0.2	0.4	0.6	0.2	0.0
86	1.2	0.5	0.8	0.3	0.0
87	1.2	0.8	1.6	0.3	0.0
88	0.1	0.5	0.6	0.3	0.0
89	6.1	14.6	14.6	18.9
90	0.2	0.5	0.6	0.2	0.0
91	5.0	1.6	1.8	18.2
92	0.2	0.4	0.6	0.2	0.0
93	0.2	0.4	0.6	0.3	0.0
94	2.5	2.5	3.2	60.0
95	0.1	0.3	0.5	0.3	0.0
96	1.2	0.4	0.9	0.3	0.0
97	0.2	0.4	0.7	18.3
98	0.2	0.4	0.7	0.2	0.0
99	0.2	0.4	0.8	0.3	0.0
100	1.3	2.3	2.8	0.3	0.0
	CSI-0.1	CSI-0.6	CSI-1.0	✔CSI-1.0	CeTA
101	0.2	0.4	0.5	0.2	0.0
102	1.3	2.3	2.8	0.4	0.0
103	2.2	0.6	0.5	0.3	0.1
104	0.1	0.4	0.7	0.2	0.0
105	6.1	1.1	0.9	28.5
106	2.4	1.1	1.3	0.3	0.0
107	1.2	0.3	0.4	18.3
108	5.2	0.3	0.6	18.3
109	60.0	60.0	5.9	60.0
110	6.1	60.0	60.0	60.0
111	1.3	0.5	0.8	0.3	0.0
112	0.9	0.5	1.0	0.3	0.0
113	0.1	0.6	0.7	0.3	0.0
114	0.3	1.1	1.4	0.3	0.0
115	0.9	1.8	2.1	0.4	0.0
116	4.2	0.9	1.6	0.3	0.0
117	6.1	1.4	1.6	18.2
118	1.8	1.6	1.9	18.2
119	1.2	0.4	0.6	18.2
120	6.1	30.7	1.3	44.4
121	1.3	0.9	1.2	0.3	0.1
122	6.1	1.2	0.9	60.0
123	6.1	0.8	1.1	60.0
124	6.1	1.2	1.8	44.7
125	6.1	1.1	1.1	60.0
	CSI-0.1	CSI-0.6	CSI-1.0	✔CSI-1.0	CeTA
126	6.1	60.0	60.0	60.0
127	4.2	1.8	1.4	60.0
128	2.4	1.0	1.4	0.3	0.0
129	6.1	1.6	1.6	37.8
130	2.2	1.0	1.4	0.4	0.0
131	2.5	1.3	1.3	0.3	0.0
132	2.8	1.1	1.0	60.0
133	6.2	1.1	1.0	60.0
134	1.9	1.6	2.0	12.6
135	0.1	0.6	1.2	0.3	0.0
136	6.1	1.3	1.1	60.0
137	1.3	1.0	1.4	0.3	0.0
138	6.1	0.9	0.9	0.4	0.0
139	6.1	47.2	3.4	42.3
140	6.1	60.0	1.5	60.0
141	2.9	1.5	1.8	8.8	8.4
142	6.1	60.0	1.3	60.0
143	6.1	60.0	0.6	60.0
144	24.2	21.2	0.8	60.0
145	60.0	60.0	2.1	60.0
146	2.4	1.2	1.5	0.3	0.0
147	2.5	1.2	0.9	60.0
148	2.5	1.0	0.9	17.2
149	1.2	0.5	1.0	0.3	0.0
150	0.1	0.6	1.0	0.3	0.0
	CSI-0.1	CSI-0.6	CSI-1.0	✔CSI-1.0	CeTA
151	6.1	1.5	1.1	60.0
152	6.1	1.7	2.1	0.5	0.0
153	2.8	1.1	0.8	20.1
154	4.0	60.0	5.0	37.4
155	60.0	60.0	1.1	60.0
156	6.1	1.3	1.3	60.0
157	6.1	1.2	1.1	26.5
158	0.1	0.7	1.1	0.3	0.0
159	2.2	1.4	1.9	0.4	0.0
160	6.2	25.5	31.0	60.0
161	6.1	0.9	1.0	27.2
162	6.1	37.8	1.4	29.3
163	1.2	0.6	0.9	0.2	0.0
164	6.1	60.0	1.6	60.0
165	1.2	1.1	1.4	0.3	0.0
166	2.4	1.0	1.3	0.3	0.0
167	1.3	0.8	1.2	0.3	0.0
168	6.1	1.4	1.6	0.5	0.0
169	6.1	60.0	34.7	25.1
170	6.1	48.0	60.0	45.2
171	60.0	60.0	1.0	60.0
172	6.3	1.2	0.8	60.0
173	6.1	14.5	14.7	60.0
174	6.1	37.6	1.8	32.0
175	16.4	60.0	3.7	53.4
	CSI-0.1	CSI-0.6	CSI-1.0	✔CSI-1.0	CeTA
176	6.1	1.7	1.9	36.7
177	1.2	0.3	0.8	0.2	0.0
178	1.2	0.6	0.7	0.3	0.0
179	0.1	0.4	0.5	0.2	0.0
180	2.5	1.2	1.6	0.3	0.0
181	6.1	1.7	1.9	43.9
182	6.1	30.7	31.0	42.9
183	6.1	39.6	1.7	60.0
184	6.1	60.0	0.8	60.0
185	6.1	42.8	1.5	60.0
186	2.4	1.0	1.5	0.3	0.0
187	6.1	40.1	1.6	37.5
188	6.1	1.3	1.1	28.7
189	6.1	1.7	2.0	41.1
190	1.2	1.0	1.3	0.3	0.0
191	6.1	60.0	1.7	60.0
192	6.1	1.0	1.0	60.0
193	6.1	1.3	1.5	17.0
194	1.2	1.3	1.7	0.6	0.0
195	6.1	60.0	1.6	60.0
196	60.0	14.0	1.7	60.0
197	2.9	1.2	0.9	18.3
198	6.1	1.1	1.1	60.0
199	2.4	1.1	0.9	26.1
200	2.5	0.9	1.4	0.3	0.0
	CSI-0.1	CSI-0.6	CSI-1.0	✔CSI-1.0	CeTA
201	2.7	1.0	0.8	2.9	2.3
202	6.1	1.3	1.2	60.0
203	60.0	18.5	6.8	60.0
204	6.1	1.5	1.8	42.7
205	0.2	0.6	1.2	0.2	0.0
206	6.1	60.0	1.3	21.8
207	2.3	1.1	1.2	0.3	0.0
208	0.6	60.0	7.2	31.5
209	6.2	1.2	1.1	28.7
210	6.1	1.4	1.2	27.9
211	2.2	0.6	0.6	0.3	0.1
212	2.2	0.6	0.8	0.3	0.0
213	2.2	0.4	0.6	0.3	0.0
214	2.8	0.5	1.1	0.5	0.0
215	2.9	0.8	1.1	60.0
216	6.1	10.6	10.6	6.3	0.2
217	6.1	1.6	1.8	60.0
218	3.0	0.4	0.6	51.2
219	2.3	0.4	0.5	18.2
220	0.1	0.3	0.5	0.2	0.0
221	2.7	0.5	0.5	51.1
222	6.2	0.4	0.6	18.2
223	1.2	0.5	0.7	0.3	0.0
224	1.2	0.5	0.6	0.2	0.0
225	0.1	0.4	0.4	0.2	0.0
	CSI-0.1	CSI-0.6	CSI-1.0	✔CSI-1.0	CeTA
226	0.2	0.3	0.4	0.2	0.0
227	6.1	14.7	14.7	18.2
228	6.2	0.5	0.6	18.2
229	0.2	0.5	0.9	18.3
230	6.2	15.7	16.1	60.0
231	6.2	14.5	14.8	18.3
232	1.8	0.4	0.7	0.2	0.0
233	6.1	0.4	0.7	0.3	0.0
234	2.4	14.5	14.5	20.6
235	6.2	0.5	0.5	0.3	0.0
236	0.1	0.4	0.4	0.2	0.0
237	0.1	0.4	0.6	0.3	0.0
238	0.1	0.5	0.6	0.2	0.0
239	0.2	0.4	0.6	0.2	0.0
240	0.1	0.4	0.6	0.3	0.0
241	0.1	0.4	0.5	0.3	0.0
242	0.2	0.5	0.6	0.3	0.0
243	0.3	0.4	0.6	0.3	0.0
244	0.1	0.4	0.6	0.2	0.0
245	60.0	0.4	0.6	0.2	0.0
246	3.7	0.4	0.6	0.2	0.0
247	60.0	0.4	0.5	0.3	0.0
248	0.2	0.5	0.5	0.2	0.0
249	60.0	0.6	0.7	0.3	0.0
250	6.1	14.6	14.6	18.5
	CSI-0.1	CSI-0.6	CSI-1.0	✔CSI-1.0	CeTA
251	60.0	0.8	0.9	0.4	0.0
252	60.0	0.4	0.5	0.2	0.0
253	60.0	0.5	0.6	0.3	0.0
254	0.1	0.4	0.5	0.2	0.0
255	1.9	0.4	0.6	0.2	0.0
256	60.0	60.0	60.0	60.0
257	60.0	60.0	60.0	60.0
258	0.8	0.4	0.6	0.2	0.0
259	2.2	1.6	2.1	60.0
260	2.4	1.8	2.2	60.0
261	0.1	0.5	0.5	0.3	0.0
392	0.1	0.3	0.4	0.2	0.0
412	6.2	0.7	1.1	0.6	0.0
413	6.1	0.6	0.6	0.4	0.0
414	6.1	60.0	60.0	60.0
415	6.2	21.8	60.0	60.0
416	6.2	0.4	0.6	0.3	0.0
417	6.1	60.0	60.0	60.0
418	6.2	0.5	0.8	0.3	0.0
419	6.2	0.4	1.2	0.3	0.0
420	6.1	0.5	0.4	0.3	0.0
421	6.1	0.4	0.7	0.3	0.0
422	6.1	0.5	0.8	0.3	0.0
423	54.2	0.4	0.6	1.1	0.0
424	1.8	0.4	0.5	0.2	0.0
	CSI-0.1	CSI-0.6	CSI-1.0	✔CSI-1.0	CeTA
425	1.9	0.4	0.5	0.3	0.0
442	2.3	2.7	1.8	0.3	0.0
496	1.2	15.5	15.6	18.8
497	6.1	60.0	14.2	10.1	0.0
498	2.2	1.8	2.2	18.2
502	1.2	0.5	0.7	0.3	0.0
503	0.1	0.3	0.6	0.3	0.0
504	0.1	0.5	0.7	0.3	0.0
505	0.1	0.3	0.4	0.2	0.0
506	0.2	0.5	0.7	0.3	0.0
507	0.1	0.4	0.5	0.2	0.0
508	0.3	0.4	0.5	0.3	0.0
509	0.1	0.3	0.5	0.2	0.0
510	0.1	0.4	0.5	0.2	0.0
511	0.2	0.5	0.5	0.2	0.0
512	0.2	0.5	0.4	0.2	0.0