[Termtools] A proposal for the next competition (towards verification)

[Johannes Waldmann]

Koprowski, A. wrote:

>  Considering Hans' proposal of making the output somehow more formal I fully agree.
> Termination tools are getting more and more complex 
> and as always with complicated software bugs happen. 
> Also the proofs itself are getting more involved 
> making it difficult to verify them by hand. 

A second step (the first step being what Hans suggested)
is that each tool should be able to check its *own* proofs,
in the following sense:

it should be able to read a problem *and* a proof
(written in the tool's *own* output format)
and decide whether it thinks the proof is correct.

What is it good for? For one thing, we could then make verifiable
claims of the sort "this is a proof that XXX could have found"
(where XXX might be some "educational" version that only has
very restricted features) and for another, this would help in debugging.
E. g. this would provide a safety measure
when porting a tool from one platform to another
(tool XXX on platform A could check a proof by tool XXX on platform B,
where A and B might mean different tool versions, compilers, OSs, etc.)

I think it should be moderately easy
to program a tool to read its own output format and check it,
at least far easier than to agree on a common output format
between several tools (it seems), so perhaps some tools' output
format(s) will emerge as standards (for certain types of proofs).

Best regards,
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------

_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools