[Termtools] Confusion on iRankFinder and AProVE

[Marcel Hark]

Dear Akihisa,

We saw that you reported an error to Aaron regarding AProVE and
iRankFinder ([1]). Also, there was some confusion about AProVE using
iRankFinder. As you said, this sounds politically delicate since in the
category "C Integer" iRankFinder and AProVE are competitors.

For the complexity analysis of integer transition systems, in AProVE's
sub-tool KoAT we use control flow refinement ([2]) to improve our
analysis. The technique presented in [2] is implemented in a part of the
tool iRankFinder and contained in its releases. Samir and Jesús (the
developers of iRankFinder) helped us with the technical intricacies to
combine our backend with this implementation of CFR. We are only using
this CFR-part of iRankFinder and we are only using it in the
(demonstration) category for complexity of ITSs.

We had asked Samir about this before the competition, and he explicitly
gave us the permission to use iRankFinder in the competition here. In
particular, we are not using any of the techniques for proving
termination implemented in iRankFinder. Note that iRankFinder itself
only participates in categories, where termination is analyzed. In those
termination categories, we do not use iRankFinder, so especially in the
category "C Integer" we do /not/ make use of iRankFinder.

Best,

Jürgen and Marcel

[1] http://irankfinder.loopkiller.com:8081/

[2]
https://www.cambridge.org/core/journals/theory-and-practice-of-logic-programming/article/controlflow-refinement-by-partial-evaluation-and-its-application-to-termination-and-cost-analysis/F3A5114B53F0D56C3A081E5D7E5F50F2

-- 

Marcel Hark
Research Group Computer Science 2
RWTH Aachen University
52056 Aachen
Germany

E-Mail: marcel.hark at cs.rwth-aachen.de"
Phone: +49-241/80-21214
Fax: +49-241/80-22217
Room: 4208, Ahornstr. 55

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20200702/8800233a/attachment-0001.htm>