Back to Gaston
1. STRAND
2. UABE
3. Generated formulae

About benchmark

Formulae of Strand benchmark are derived fromt he WS1S-based shape analysis of [1] that contains various invariants over structures like single-linked lists or bubble sort algorithm.

Machine Specification

Operating system:	Debian GNU/Linux
Processor	Intel Core i7-4770@3.4GHz
Memory	32 GiB RAM

Discussion

For this set of experiments, we considered MONA, dWiNA and Gaston only since other tools were missing some of the features (e.g. atomic predicates) needed to handle the formulae.

The formulae of Strand have narrow quantifiers (i.e. contains lesser number of bounded variables), but on the contrary have larger quantifier nesting. In our experience, treating MTBDD nodes as automata states (denoted as Heuristic II), presented in the paper, is not efficient for this benchmark. The explicit generation of symbols (Heuristic I) is however powerful and Gaston is mostly comparable, in two cases better and in one case worse than MONA (note that we are currently investigating why the given formula is exploding in our approach).

Used notations

∞	the running time exceeded 2 minutes
oom	the tool ran out of memory
k	k quantifier alternations were added to the original benchmark
N/A	benchmark required some feature or atomic predicate unsupported by the given tool
All	Overall number of generated unique terms (e.g. DAG nodes)
Fixpoint	Overall number of terms inside computed fixpoint
MONA	State space generated by MONA on the leaf levels of the terms

Experimental results

benchmark	MONA		Gaston (Heuristic I)				Gaston (Heuristic II)				dWiNA
	Time [s]	Space [states]	Time [s]	Space [states]			Time [s]	Space [states]			Time [s]
				All	Fixpoint	MONA		All	Fixpoint	MONA
strand-new-bubblesort-else.mona	0.02	14469	0.01	2138	2680	1787	0.05	9715	609745	2142	∞
strand-new-bubblesort-if-else.mona	0.11	61883	0.03	3207	3076	2870	0.15	16296	2027176	3269	∞
strand-new-bubblesort-if-if.mona	0.28	127552	0.09	5428	5649	5062	0.42	29189	7261360	5483	∞
strand-new-sorted-list-insert-after-loop.mona	0.01	2634	0.20	5066	30568	631	9.90	70044	6471433	631	50.06
strand-new-sorted-list-insert-before-head.mona	0.01	678	0.01	541	614	274	0.01	1843	14837	296	0.84
strand-new-sorted-list-insert-before-loop.mona	0.01	1448	0.01	656	310	486	0.01	1590	9856	552	20.31
strand-new-sorted-list-insert-error-error.mona	0.01	1448	0.01	656	310	486	0.01	1590	9856	552	20.28
strand-new-sorted-list-insert-in-loop.mona	0.01	5945	0.01	1079	675	845	0.01	3599	65074	1008	∞
strand-new-sorted-list-reverse-after-loop.mona	0.01	1941	0.01	579	309	422	0.01	1820	14818	510	12.74
strand-new-sorted-list-reverse-before-loop.mona	0.01	1941	0.01	579	309	422	0.01	1820	14818	510	12.82
strand-new-sorted-list-reverse-in-loop.mona	0.03	23349	0.01	3247	2082	2834	0.06	12006	725582	3130	16.24
strand-new-sorted-list-search-after-loop.mona	0.01	1072	0.01	419	210	287	0.01	1159	5785	353	2.31
strand-new-sorted-list-search-before-loop.mona	0.01	1181	0.01	510	245	362	0.01	1323	7293	428	47.25
strand-new-sorted-list-search-in-loop.mona	0.04	23349	0.01	3247	2082	2834	0.05	12006	725582	3130	16.23

Acknowledgement

We thank authors of STRAND tool (P. Madhusudan, X. Qiu and G. Parlato) for publication of their experiments with WS1S formulae.