Gaston

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

About benchmark

Formulae from the UABE benchmark are from the recent work~[1], which uses WS1S to reason about programs with unbounded arrays.

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.

Some of the formulae have wide quantifiers (i.e. contains larger number of bounded variables) and the former version of Gaston had problems even just with the generation of required symbols (e.g. for quantifier with 10 variables 2^10 symbols are needed) resulting in large number of timeouts as seen in (Heuristic I) column in the table. We have thus optimized the state space search to treat MTBDD nodes as automata states to handle such formulae, denoted in table as (Heuristic II). In this setup, Gaston outperformed MONA on seven out of twenty-three benchmarks, it was worse on ten formulae and comparable on the rest. These results confirm that our approach can defeat MONA in practice, however, still lacks some further optimizations as we discussed in the paper.

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
array_axiom.mona 1.51 30253
ex1.mona 0.01 481 0.01 305 12 296 0.01 303 12 296
ex10.mona 6.92 131835 11.82 82236 5368930 572
ex11.mona 4.04 2393 0.05 5743 4785 835 0.1 4156 103736 835
ex12.mona 0.11 2591 5.4 68159 1916257 888
ex13.mona 0.01 2601 0.87 16883 2033094 470
ex14.mona 0.04 3140 0.01 2689 18481 836
ex15.mona 0.01 242 0.01 105 0 103 0.01 105 0 103
ex16.mona 0.01 3384 0.18 3960 730322 813
ex17.mona 3.15 165173 0.09 3952 68646 657 0.08
ex18.mona 0.18 19463
ex19.mona 0.01 2933 0.05 3411 2614 1856 0.04 6854 90341 1856
ex2.mona 0.1 26565 0.01 1773 218 1644 0.01 1841 1210 1644
ex20.mona 1.26 1077 0.1 14258 454 840 0.21 12266 189265 840
ex21.mona 1.51 30253
ex3.mona 3.77 194856 3.43 181897 2777173 175212
ex4.mona 0.03 6797 0.33 22442 977296 4220
ex5.mona 0.01 1296 0.01 3301 23792 1082 12.89
ex6.mona 3.69 27903 21.44 132848 10104634 41819
ex7.mona 0.75 857 0.01 463 25 365 0.01 594 288 365 0.01
ex8.mona 6.83 106555 0.01 1618 932 1045 0.01 1624 41941 1045 42.46
ex9.mona 6.37 583447 8.38 411997 385 411627 8.31 412417 5047 411627
fib.mona 0.04 8128 22.15 128688 6068021 6924

Acknowledgement

We thank authors of UABE prototype tool (Min Zhou, Fei He, Bow-Yaw Wang, and Ming Gu) for sending us their benchmark WS1S formulae.


  1. Min Zhou, Fei He, Bow-Yaw Wang, and Ming Gu. Array theory of bounded elements and its applications.