Papers
David Sabel and
Hans Zantema.
Termination of cycle rewriting by transformation and matrix
interpretation.
Logical Methods in Computer Science, Volume 13, Issue 1,
March 2017.
[
bib |
DOI |
http ]
David Sabel and
Hans Zantema.
Transforming Cycle Rewriting into String Rewriting.
In Maribel Fernández, editor,
26th International Conference
on Rewriting Techniques and Applications (RTA 2015), volume 36 of
Leibniz International Proceedings in Informatics (LIPIcs), pages 285-300,
Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer
Informatik.
[
bib |
http |
DOI |
PDF (extended version) |
slides (RTA 2015)
]
David Sabel and
Hans Zantema.
TermComp 2016 Partipicant: cycsrs 0.2.
In Aart Middeldorp and René Thiemann, editors,
Proceedings of the 15th International Workshop on Termination, Obergurgl, Austria, pages 21:1, 2016.
[
http ]
Experimental Results
Benchmarks for cycsrs-0.2.0.5, September 2016
We performed several experiments on
StarExec.
The results and job information can be found via the linked job pages on
StarExec.
Termination and Complexity Competition 2016
Our tool cycsrs participated in the
Cycle Rewriting category in the
Termination and Complexity Competition 2016
which was affiliated with
15th International Workshop on Termination.
The results from the competition are available
here
which were run on
StarExec, the original job can be found
here.
Benchmarks for cycsrs-0.2.0.0, April 2016
To benchmark the updated version of cycsrs, we performed several experiments on
StarExec.
The results and job information can be found via the linked job pages on
StarExec.
Termination Competition 2015
Cycle Rewriting became a new category in the
Termination Competition 2015
which was affiliated with
CADE-15.
Our tool cycsrs (using many other termination and deduction tools) participated in the new category.
The results from the competition are available
here
which were run on
StarExec, the original job can be found
here.
Results obtained for the RTA 2015 paper
We tried to prove cycle termination of several problems using our developed techniques.
An overall
summary of the experiments can be found
[here].
The detailed results for the following three problem sets can be found on separate webpages:
- The results of proving cycle termination of the 1315 problems of SRS_Standard-branch of the Termination Problem Data Base can be found
[here]
- The results of proving cycle termination of 50000 randomly generated problems of size 12 over an alphabet of size 3 can be found [here]
- The results of proving cycle termination of some selected (and some quite hard) problems, including examples from the paper, are collected [here]
Due to their large size not all termination proofs generated by termination provers are included on the corresponding websites, but they can be downloaded
as a single compressed tar-archive
[here] (compressed size ~1,2GB, uncompressed ~26GB)
Downloads
torpacyc
The recent version of
torpacyc (developed by Hans Zantema) can be download from
this webpage.
Command line tool cycsrs (Version 0.2.0.5)
The new version of the command line tool cycsrs to transform cycle rewriting systems into string rewrite systems and to
prove cycle termination by different tools is available as:
It includes also the sources of the cycle non-termination checker cycnt and the cycle termination prover
tdmi which searches for trace decreasing matrix interpretations using SMT-solvers.
Type
cycsrs help for a detailed usage information.
The tool can perform the transformations without any further tools, but for proving cycle termination
the termination provers torpacyc, AProVE, and TTT2 (and their dependencies) are required to be installed.
See the
README for detailed explanations.
Changes for 0.2.0.5 compared to version 0.2.0.2:
- The cycle nontermination checker was improved
Changes for 0.2.0.2 compared to version 0.2.0.0:
- A bug in the cycle nontermination checker was fixed.
Changes compared to version 0.1.0.0:
- torpacyc 2014 is no longer available (torpacyc 2015 remains)
- several cycle termination techniques are extended for relative cycle termination
- a new cycle non-termination checker cycnt is included and can be called from cycsrs
- a new cycle termination checker tdmi is included and can be called from cycsrs, it searches
for trace-decreasing matrix interpretations using the normal, tropical and arctic semi-ring.
It targets QF_BV of
SMT-LIB and thus can be used with different SMT-solvers.
- tdmi and cycnt are ready to use for relative cycle termination
- configuring the tool chain and distributing time limits on the several chain is more comfortable
- the source code was heavily rewritten, using the concept of non-/termination processors to allow for a more modular design
Command line tool cycsrs (Version 0.1.0.0)
The command line tool to transform cycle rewriting systems into string rewrite systems and to
prove cycle termination by different tools is available as:
Type
./CYCSRS help for a detailed usage information.
The tool can perform the transformations without any further tools, but for proving cycle termination
the termination provers torpacyc, AProVE, and TTT2 (and their dependencies) are required to be installed.
See the
README for detailed explanations.