This page collects experimental results conducted with
our amortised resource analysis (ARA) in combination with the complexity analyser TcT,
version 3.2:
All experiments were run with a timeout of 60s on a machine with an Intel(R) Core(TM) i7-7700 CPU @ 3.60GHz and 16GB RAM. For the TPDB testbed we used the runtime-complexity subset of the termination problem database, version 10.4.
- Experimental evaluation on the TPDB testbed
- Experimental evaluation on the TRS testbed
- Experimental evaluation on the HOCA/RAML testbed
Legend:
- TcTAra: TcT competition mode with the possibility to use ARA wherever polynomial interpretations are allowed as well
- TcTNoAra:TcT competition mode without ARA
- AraTRS: Standalone ARA without cost-free derivations (CF) directly on the TRS
- AraTRSHeuristics: Standalone ARA with heuristics enabled only working directly on the TRS
- AraTRS CF/AraTRSCostFree: Standalone ARA with cost-free derivations (CF) directly on the TRS
- AraHoca: Standalone ARA without cost-free derivations (CF) working on OCaml code. This allows the use of type information provided from the OCaml code which is utilized in the heuristics.
- AraHocaCostFree: Standalone ARA with integrated transformation of OCaml to TRS. This allows the use of type information provided from the OCaml code which is utilized in the heuristics.
- TcTHoca/TcTHocaARA: TcT-Hoca competition mode with integrated transformation with ARA enabled.
- TcTHocaNoAra: TcT-Hoca competition mode with integrated transformation without ARA enabled.
- Raml-1.4.2: Latest available version 1.4.2 (May 2019) of Raml, which works on OCaml code directly.
- Aprove: Latest version (May 2019) of AProVE, which works with the strategy of the latest termination competition (2018)
All experiments were run with a timeout of 60s on a machine with an Intel(R) Core(TM) i7-7700 CPU @ 3.60GHz and 16GB RAM. For the TPDB testbed we used the runtime-complexity subset of the termination problem database, version 10.4.