[Termtools] timeout for verification: 1 minute

[Frederic Blanqui]

Julien, these are just statistics. Every one can interpret these 
statistics as he/she wants. It is not intended to say that one approach 
is better than another one. But it can help in comparing these 
approaches objectively.


Julien Forest a écrit :

>> 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 
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools