Termination Competition 2014 technical details

We intend to run the competition on StarExec - a cross-community solver execution and benchmark library service under joint development (since 2012) at the University of Iowa and the University of Miami. Its goal is to facilitate the experimental evaluation of logic solvers and other automated reasoning tools by providing a shared storage and computing infrastructure to store, manage and make available benchmark libraries; execute comparative evaluations; and run solver competitions.

For displaying the results of the termination competition, we are building a separate web service at HTWK Leipzig.

Here is some information for participants:

• submit solvers for testing the platform [1]
• how to register on starexec [2] NOTE: there may be service interruptions (e.g., sudden changes in benchmark arrangement).
• STAREXEC_MAX_MEM only 750 MB? [3] (UPDATE: this was out of date, the limit is actually 64 GB)
• Beware if your solver writes to stderr. The "postprocessor" (that expects YES|NO in the first line, for termination) gets to see stdout and stderr merged. If you have trace/log output, you can only show it after the actual answer.
• hardware on starexec: see [4] Solvers are run on nodes with 4 cores each.
• software on starexec: RHEL 6.3 (so Centos 6.3 should be a close match). Package selection, see [5]
• java is available on starexec nodes (jdk 1.6.0_41) - see [6] - see also remark on ulimits and -Xmx [7]
• it is helpful to follow other solver communities, e.g., SMT COMP 2014
• solvers will be called with the file name of the termination problem as the only argument. Solvers can read environment variables to enquire about timeout (and other parameters), cf. https://wiki.uiowa.edu/display/stardev/User+Guide#UserGuide-SpecialVariables

information on the web GUI (under construction) for presenting results Star_Exec_Presenter

Separate page with impressions from using the demo version of Star Exec, in 2012: Star_Exec_Test