Gaston

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

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.