[Termtools] Confusion on iRankFinder and AProVE

[Yamada, Akihisa]

Dear Marcel,

thanks for clarification, the dependency graph looks complicated :)

Best,
Akihisa

On 2020/07/02 17:32, Marcel Hark wrote:
> 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
> 
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
> 

-- 
このEメールはアバスト アンチウイルスによりウイルススキャンされています。
https://www.avast.com/antivirus