[SMT-COMP] about to start the competition - information and actions for competitors

[Matthias Heizmann]

Hi David,

thank you for your regular reports about the current state of the SMT-COMP 
2014.

On the SMT-COMP website I can see how each solver performed in each category. 
However, I would also like to see how each solver performed on individual 
benchmarks (especially on the benchmarks that I contributed).

Is there a way to get this information?

Matthias






On Monday 16 June 2014 12:53:08 David Cok wrote:
> Non-competitors: The relevant piece of information for you is that
> progress will be available at
> smtcomp.sourceforge.net/2014/results-toc.shtml (these pages will be
> improved as well as updated with progress as the competition proceeds).
> 
> SMTCOMP competitors:
> 
> Thanks for all of the work - some late last night - to get all the
> solvers in. Here is some information and some things for you to do.
> 
> 1) I tried to carefully sort through the flood of email, but I may have
> missed something. So check the entries for your solvers on the
> participants web page - be sure I have recorded the correct solver and
> configuration (and divisions). If there are any typos in names etc. feel
> free to point them out as well.
> 
> 2) You now have time to complete a solver description, if you have not
> already sent me one. If there is a ? in the column for solver
> description on the participants table, I don't have one from you (or I
> don't know that I have it).
> 
> 3) I have given the competitors permission to see the submitted solvers
> and the competition space.  It is under
> "Competitions and Evaluations"/SMTCOMP2014/Competition and "Competitions
> and Evaluations"/SMTCOMP2014/Solvers . Don't change anything there, if
> by mistake you have permission to do so. If you can't see it, let me know.
> 
> 4) You will note that the competition is divided into heats. We are
> unsure of how long the computations will take, in part because we have
> many new submissions. So we will do 1000 benchmarks for each division
> first (if there are that many), and then the next 1000, etc. Each heat
> was chosen according to the rules from any benchmarks left after
> previous heats have been removed. We will progress all divisions
> equally, with the exception that we will attempt to complete all
> benchmarks of QF_BV. If the competition ends with some heats for some
> divisions not completed, no data from the uncompleted heats will be used.
> 
> 5) Because of the heats and the many divisions, StarExec does not give
> an easy overall view of the competition's progress. We have put together
> some web pages summarizing the status. These will be refreshed as the
> competition progresses (around the clock, once I find a place other than
> my laptop to do the computations). You may have to empty the cache on
> your browser regularly to see the progress. The progress page is linked
> off the smtcomp website at
> smtcomp.sourceforge.net/2014/results-toc.shtml .
> 
> 6) We will use a timeout of 40 minutes wall and cpu time per benchmark.
> Some of our estimates suggest that we could extend beyond this, but we
> are unsure of how much overhead time there will be, or restarts, or our
> own fumbling with StarExec.
> 
> 7) We are still working through recusing the benchmarks that depend on
> the semantics of divide-by-zero, per the earlier discussion. We may
> start the competition jobs anyway and remove the benchmarks at issue
> after the fact.
> 
> 8) We had two withdrawals, because of bugs that could not be fixed in
> time. If those solvers are submitted late, we will accept them as
> non-competitive entries. The same is true for any currently entered
> solver that is resubmitted because of a bug found during competition.
> 
> 9) As previously stated, we will attend to the application track once we
> have the main track underway. More about that later.
> 
> 10) If you see something amiss, by all means email.
> 
> The organizers.
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 836 bytes
Desc: This is a digitally signed message part.
URL: </pipermail/smt-comp/attachments/20140620/cb5f8aec/attachment.asc>