June 2024 - Termtools - lists.rwth-aachen.de

First Run(s), Demo Categories
by Florian Frohn 28 Jun '24

28 Jun '24

3 3

no more updates, certificates
by Florian Frohn 28 Jun '24

28 Jun '24

Dear all, I created the Jobs for the final run. So from now on, I'll only accept updates for very good reasons. I'll start the first jobs as soon as we have a screen to display the results at IJCAR. You can check the current state of the competition here: https://termcomp.verify.rwth-aachen.de/Y2024/ There, you can also see the configurations that are registered for your tool. Please make sure that they are correct. This year, we'll have certificates for all winners, and I'll hand them out during the termCOMP session (Friday, 17:30). So if you attend IJCAR and participate in one of the competition categories, make sure you're there! If you don't attend IJCAR, please ask someone else to (maybe) pick up your certificate for you. If you don't expect to win, note that there will also be some special prices, so please (ask someone to) attend the session anyway. Best Florian

1 0

termCOMP at IJCAR
by Florian Frohn 26 Jun '24

26 Jun '24

1 0

Testing done
by Florian Frohn 26 Jun '24

26 Jun '24

Dear all, the testing for the competition categories is over. Some tools still have problems regarding their performance (rejects in certified categories or severe regressions compared to last year), but from a technical point of view, all tools (*) are working. If your tool has rejects or significant regressions, then you've been notified. I'll continue to accept updates, but I won't run any more tests. So if you update your tool, please make sure that the updated version works on StarExec. Moreover, the links to the proofs in the demo categories are working again. Best Florian (*) AutoNon still has a few issues, but that's a 'historical' tool that was just registered for reference. I'll take care of updating it.

1 0

new post-processors
by Florian Frohn 24 Jun '24

24 Jun '24

1 1

registration is over
by Florian Frohn 21 Jun '24

21 Jun '24

Dear all, the registration for termCOMP is over. Some teams worked really hard to fix issues caused by the StarExec update, resulting in some last minute registrations. Thanks for that! If you missed the deadline, but intended to participate, please get in touch. Best Florian

1 0

BenchExec no longer available
by Florian Frohn 21 Jun '24

21 Jun '24

Dear all, I was just informed that the benchmarking framework that we used in the past (BenchExec) is no longer available on StarExec. Hence, we'll have to work with "runsolver" instead. If I remember correctly, we used runsolver at some point, but then we switched to BenchExec due to issues with the measurement of the runtime. If you remember any details / your tool was affected by these problems, please let me know. Best Florian

2 7

ceta(2) - selective context closure?
by Johannes Waldmann 17 Jun '24

17 Jun '24

Dear all, can I express in CPF (for Ceta-2) that I want to apply "flat context closure" to a subset of rules only? specifically, I want this for rules with empty lhs or rhs, as it seems to increase the power of matrix interpretations. (as shown by Aprove in TC 23). I am looking at http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/825022… but the example seems to close all rules. I guess I can indeed context-close all rules uniformly, and use the same interpretation, to remove the same rules. But perhaps I want other methods that refer to the original rules. Well it's a bit late anyway. - J.

2 2

Postprocessors for certified categories
by Florian Frohn 14 Jun '24

14 Jun '24

2 1

CPF version
by Florian Frohn 13 Jun '24

13 Jun '24

Dear all, just to clarify, we expect the tools to output *CPF2 proofs* in the certified categories (just like last year). If your tool already supports the new CPF3 format and you planned to make use of that at termCOMP, please let me know. Best Florian

1 0