[SMT-LIB] Updates on SMTCOMP 2014

[Tim King]

Hi Bruno,

Here are the relevant links for registration:
https://www.starexec.org/starexec/public/registration.jsp
https://wiki.uiowa.edu/display/stardev/User+Guide#UserGuide-Registration

You will also likely want to read the section on the User's Guide for
Solvers. Uploading a solver is a little tricky, but is nicely documented
there.  A lot of good information on common problems is also available on
the forums:
http://starexec.forumotion.com/

Aaron tends to post the most up to date information about the status of the
cluster (restarts, etc.) on the StarExec blog:
http://starexec.wordpress.com/

--Tim

On Wed, May 28, 2014 at 2:00 PM, Bruno Dutertre <bruno.dutertre at sri.com>wrote:

> 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
>>
>>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>