Empirical Evaluation
We have implemented our approach for the automated termination analysis of
CERSs and CS-CERSs in the termination prover
AProVE, resulting in
the system AProVE-CERS. For the results recorded below, AProVE-CERS was run
on an AMD Athlon™ processor running at 2.2 Ghz. For each example, a
time limit of 60 seconds was imposed. All times are in seconds.
Context-sensitive examples
The collection of examples consists of examples from context-sensitive
category of the
Termination Problems Data Base 5.0.2, suitably adapted to make use of
built-in integers and collection data structures.
Non-context-sensitive examples
The collection of examples includes examples from the literature that were
again suitably adapted to make use of built-in integers and collection data
structures. Additionally, several examples were obtained from imperative
programs encoded into rewrite rules.
Additionally, AProVE-Integer (which is based on the methods of the paper Proving
Termination of Integer Term Rewriting) has been run on the subset of
examples where it is applicable. An "N/A" in the AProVE-Integer column
means that AProVE-Integer is not applicable to that rewrite system.