[SMT-LIB] Updates on SMTCOMP 2014

[Bruno Dutertre]

On 05/28/2014 09:20 AM, David Cok wrote:
> 1) The competition website has been updated to include a participants page, where details of those participating (so far, mostly, intending to participate) in the competition are listed. This will be updated as we receive official submissions: http://smtcomp.sourceforge.net/2014/participants.shtml
>
> 2) Solver authors: Reminder - the preliminary deadline is *June 1*. (The final deadline is June 15.) Upload your solver to StarExec and send the organizers an email stating
> - the StarExec solver id
> - whether you are participating in the main track or application track or both (may be different solver ids)
> - the logics in which you are participating (see the note below on benchmarks)
> - a random seed
> - a solver description (can be submitted later)
> - who to contact if there are problems.
> As soon as we can we will be running trials on the solvers and benchmarks. While we are not a testing service, we will report to the contact any problems (e.g., crashes, anonymous results, failures to run, ...) we happen to discover during the run up to the final submission deadline.
>

Seems like this requires every participant to obtain an account on StarExec,
but I couldn't find how to do it on the StarExec site. Any pointer?

Thanks,

Bruno

> 3) Benchmarks. We (+ Clark Barrett) have received and curated many new benchmarks. In particular, some logics have benchmarks that did not before and we will run competitions in those divisions. See the list of logics on the participants page: http://smtcomp.sourceforge.net/2014/participants.shtml. The new logics are: BV, UFBV, QF_ABV, QF_UFNIA . We will make the new benchmark subspace public as soon as we finish the last few benchmarks sets, with the goal being this coming weekend. The following task will be creating the subset and difficulty ratings from which the competition benchmark set will be selected.
>
> 4) Rules. A final update to the rules will be in place by this coming weekend.
>
> 5) Separation Logic. A subcommunity researching SMT solvers for Separation Logic is holding an SL-SMTCOMP, with several solvers and a set of benchmarks in SMTLIBv2 format. The SMTCOMP organizing committee will run this competition as a demonstration alongside the regular SMTCOMP. Over the next year, we expect the SL community and the SMTLIB coordinators to settle on an appropriate theory, logics, benchmarks and relationship to classic SMTLIB.
>
> - David
> for the organizers
>
>
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>