This page contains additional material for the following paper:
V. Schuppan and L. Darmawan: Evaluating LTL Satisfiability Solvers. In: T. Bultan, P.-A. Hsiung (eds.): Automated Technology for Verification and Analysis - 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings. Volume 6996 of Lecture Notes in Computer Science, pp. 397-413. Springer, 2011. Download: publisher, preprint (zipped), full (zipped)
This file contains the raw data of the main stage of our evaluation.
The following documents collect additional tables and plots of our data from the main stage of our evaluation.
Link | Size | No. Pages | |
---|---|---|---|
Tables of aggregated perfomance data | 16 MB | 689 | |
Cactus plots | 163 MB | 14556 | |
Line plots | 229 MB | 14556 | |
Scatter plots - non-negated versus negated versions | 38 MB | 4931 | |
Scatter plots - model construction disabled versus enabled | 12 MB | 1312 | |
Scatter plots - winning configurations | 44 MB | 4777 | |
Scatter plots - tools (no TRP++) | 125 MB | 13401 | |
Scatter plots - tools (TRP++ s, r) | 127 MB | 14171 | |
Scatter plots - tools (TRP++ no s, r) | 127 MB | 14171 | |
Scatter plots - tools (TRP++ no s, no r) | 125 MB | 14171 |
The following table provides links to the sources of our benchmarks as well as to archives containing the benchmarks in the formats of the respective solvers. This file contains all families in all formats.
Benchmark Family | Homepage | Archive for | |||||
---|---|---|---|---|---|---|---|
ALASKA | LWB | NuSMV | pltl | TRP++ | TSPASS | ||
acacia | Link | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | alaska | Link | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | anzu | Link | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | forobots | not available | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | rozier | Link | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | schuppan | not available | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | trp | Link | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 | tar.bz2 |
ALASKA, LWB, NuSMV, pltl, TRP++, TSPASS.
This work was partly funded by the Provincia Autonoma di Trento (project EMTELOS).
© Viktor Schuppan Last modified 2 October 2011 |