Download pasta
A i386 Linux executable of pasta can be downloaded here. A recent version of Yices has to be available and
accessible in the PATH.
Start it with pasta filename, where the file filename
contains a PA-based TRS. The following example shows the syntax:
eval_1(x, y) -> eval_2(x + 1, 1) [ x >= 0 ]
eval_2(x, y) -> eval_2(x, y + 1) [ x >= 0 /\ y > 0 /\ x >= y ]
eval_2(x, y) -> eval_1(x - 2, y) [ x >= 0 /\ y > 0 /\ x < y ]
Empirical Evaluation
We have implemented our approach for the automated termination analysis of
PA-based TRSs in the prototype termination prover pasta. For
comparison, we also ran AProVE
Integer on the same set of examples. For AProVE, a timeout of one
minute was imposed.
The results recorded below were obtained on an AMD Athlon™ processor
running at 2.2 Ghz.
Notice that pasta is orders of magnitude faster than AProVE (a
total/average of 1.91s/0.05s versus a total/average of 323.09s/8.08s).
Furthermore, pasta is slightly more powerful than AProVE on this
set of benchmarks.