[Termtools] testing starexec for termination

[Johannes Waldmann]

Dear all,

I could use one or two (TRS/SRS) termination/complexity
provers/certifiers for testing on starexec.

The subject of the tests is not the termination prover,
but the platform: how to run a competition there, how
to collect and present results data. I will have a student
working on this. For that, I want to generate some test data.

For now I am using some version of Matchbox
(written in Haskell, compiled, dynamically linked executable)
and it'd be good to have some that use other technology (Java, ocaml).
Of course it can be some old version,
with a very "stupid" configuration etc.

For specification of the platform, see
https://wiki.uiowa.edu/display/stardev/User+Guide#UserGuide-Solvers
Here is the matchbox package:
http://www.imn.htwk-leipzig.de/~waldmann/termination/
I noticed that starexec machines have rather old libc
(so, Centos and not Fedora)

I am not sure how Aaron is handling accounts on starexec,
I guess you'd have to ask him if you prefer to do your own testing.
But, as I said, for now I want to test the platform
(and our programmatic access to it), not the solvers.

Thanks - Johannes.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 246 bytes
Desc: OpenPGP digital signature
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20140221/328f14c7/attachment.pgp>