[Termtools] Results for certified categories.

[Adam Koprowski]

   Dear all,

  I started browsing through the results of the certified categories of the
last termination competition and my findings are rather unnerving.

  To begin with the score of AProVE-cert in the TRS category says 594 (it's
just an example, I believe this problem concerns all the tools). However
after downloading all the results and grepping through them I could only
find 520 successful proofs. I counted 74 certification timeout in the table,
so it seems that the systems where certification timed-out are still counted
as successful proofs. This seems to be a problem on the part of the
termination competition platform.

  Even more serious is the case of cime3 in the SRS category. Its score
there says 690. That's quite suspicious given that the score of the best
prover, TTT2, in the SRS-non-certified was only 512. And indeed looking the
results table seem to indicate that cime3 could prove termination of
tpdb-5.0/SRS/Bouchare/08.srs<http://colo5-c703.uibk.ac.at:8080/termcomp/tpdb/tpviewer.seam?tpId=9388&cid=99066>and
tpdb-5.0/SRS/Bouchare/09.srs<http://colo5-c703.uibk.ac.at:8080/termcomp/tpdb/tpviewer.seam?tpId=9389&cid=99066>,
two SRSs that are non-terminating. In the certificates generated by cime I
could not find any indication of a failure, which could mean that this is a
problem of cime verification itself. That would be very worriesome indeed.
Or am I just missing something?

  I'm looking forward to comments on those findings.

   Best wishes,
   Adam

-- 
=====================================================
Adam.Koprowski at gmail.com, http://www.cs.ru.nl/~Adam.Koprowski
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.lri.fr/pipermail/termtools/attachments/20090330/2185605d/attachment.htm