[Termtools] SRS-standard-certifying

[olivier.pons]

Dear all,

We would like cime3 to be disqualified *for the SRS-standard-certifying
category ONLY*.

Indeed a quick and easy look at a certificate shows that the trs being
proved is not equivalent to the initial srs. This is due to an
ERRONEOUS VERSION OF OUR SRS PARSER. The proofs we generate are correct
but they prove the termination of a wrong trs.

As the problem does not comes from the certification process and as the
parser for trs is different this problem should not happen for trs
certification. So we want to continue the competition in the
TRS-standard category.

Best regards,

Olivier

Johannes Waldmann wrote:
> Well it appears that Cime3 proves SRS/Bouchare/08 + 09 terminating
> and gets this verified (!) while clearly these systems are looping.
> 
> Then, there are verification failures (for terminating systems) for Aprove.
> 
> Also, I am very much surprised that Cime3 proves Endrullis/08 terminating -
> this is open for some time, and I know that at least Jörg, Dieter and me
> have burnt several hours (days) of CPU + brain time trying to solve it.
> 
> Note: at this point, I am not implying anything,
> and I am not suggesting to take any action
> (I think this would require committee discussion and voting).
> I am just curious about what I see,
> and I ask the teams to provide some information.
> 
> Then I note that the category seems to be stopped
> (last result is from today, Saturday 7:59 a.m.)
> Why is this? Is it related to the points above?
> 
> Johannes.
> 
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools