[Termtools] timeout for verification: 1 minute

[Julien Forest]

Dear all, 


On Tue, 04 Nov 2008 09:57:10 +0800
Frederic Blanqui <frederic.blanqui at inria.fr> wrote:

> Then, I suggest to have a second round for the certified categories,
> either inside or outside the competition, with a 10 minutes timeout,
> but  only on  those problems  that have  not been  checked  within 1
> minute. What do you think? Would it be possible to automate this?

Those statistics  shoud be very  interesting.  Some problems  are very
hard to certify  (that was the reason why, last year,  a time limit of
10 minutes have been taken) and  it can be very interesting to be able
to see WHAT we can certify  independently from any matters of time nor
memory even if,  obviously, the results can not  be taken into account
in the competition results.

> I also suggest to provide statistics about the size of the generated
> Coq files (in Ko).

This time,  I totally  disagree with Frederic  since, the size  of the
generated .v (or the .vo) does not matters. This size depends on three
main factors:

1 -  The "size" of the considered  TRS in terms of  numbers of symbols
and rules. This size does not depend on the proof style adopted by the
certifying method  (namely ColoR/Rainbow or Coccinelle/CiME).   

2 - The criterion used by the automatic prover. If one can prove a TRS
to  be terminating  using Manna  and Ness  method, the  proof  will be
obviously much  more concise  than a proof  for the same  system using
many DP graph criteria steps (have  a look to the outputs of automatic
provers).

3- The size  of the generated .v (and .vo) file  mainly depends on the
proof style  adopted. Rainbow/Color has adopted a  deep approach while
CiME/Coccinelle  has  adopted, for  its  termination  part, a  shallow
approach. This  implies that  the proofs generated  by CiME  will have
much more lines of Coq than the ones generated by Rainbow and probably
that .vo  will be bigger (even  if I haven't checked  this part). This
comes in particular from the fact  that we have made the choice not to
prove the DP graph criterion in  Coccinelle since we think that such a
proof will need  a too complex development for  the benefits we should
obtains : the  premises of this criterion are almost  as complex as to
satisfy than the proof of the criterion itself on a particular TRS.


Best regards, 
Julien