[Termtools] Naive comments from an occasional visitor

[Carsten Fuhs]

Dear Claude,

Am Montag, 10. November 2008 16:08:01 schrieb Claude Marché:
> Claude Marché wrote:
> > Dear all,
> >
> > I'm happy to see the new competition running now! I have a couple
> > of "naive" remarks.
> >
> > In previous years, it was possible to get information on the tools
> > by clicking on their name in the first row. With new interface I'm
> > unable to get this info: who are the authors of the new tools ?
> > Where is it developed? is there a web page ?
>
> Additionally: what is the difference between Aprove-a3pat,
> aprove-cert, Aprove-color ? This info should be given to occasional
> visitors.

here, the idea is as follows:

AProVE-A3PAT is configured to use only techniques that can be
certified using the Coccinelle library and invokes CiME3 to translate
the XML-proof to Coq.

AProVE-CoLoR is configured to use only techniques that can be
certified using the CoLoR library and invokes Rainbow to translate
the XML-proof to Coq.

AProVE-Cert tries to benefit from the combined power of both certifiers: 
Here, the above two special versions of AProVE are invoked in parallel. 
As soon as one of these two instances of AProVE succeeds in finding a 
proof, the other one is terminated and the proof is certified using the 
respective Coq library. This way, we can benefit nicely from the 
parallel architecture used in the competition.

The background for this is that the techniques supported by the 
competition versions of Coccinelle and CoLoR are incomparable: 
Coccinelle uses unification for the dependency graph as opposed to the 
head symbol comparison used in CoLoR, whereas CoLoR supports arctic 
matrices. Hence, this combined setting should allow for at least as 
many (and hopefully more) certified proofs as either of the two other 
versions of AProVE participating in the certification categories would 
obtain on their own.

Best regards,

  Carsten
-- 
Carsten Fuhs          mailto:fuhs at informatik.rwth-aachen.de
LuFG Informatik 2     http://verify.rwth-aachen.de/fuhs
RWTH Aachen           phone: +49 241 80-21241