[SMT-COMP] SMT-COMP 2018: Call for Comments, Benchmarks, Solvers

[Clark Barrett]

Please refer to the instructions here for submitting new benchmarks:

https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-tmp/benchmarks-pending

On Sat, Mar 17, 2018 at 4:50 AM, Paulo Matos <pmatos at linki.tools> wrote:

> What's the procedure for the submission of new benchmarks?
>
> Kind regards,
>
> Paulo Matos
>
> On 16 March 2018 17:30:02 CET, Tjark Weber <tjark.weber at it.uu.se> wrote:
> >======================================================================
> >
> >    13th International Satisfiability Modulo Theories Competition
> >                            (SMT-COMP'18)
> >
> >                          July 12-13, 2018
> >                             Oxford, UK
> >
> >                          CALL FOR COMMENTS
> >                         CALL FOR BENCHMARKS
> >                     PRELIMINARY CALL FOR SOLVERS
> >
> >======================================================================
> >
> >SMT-COMP is the annual competition among Satisfiability Modulo Theories
> >(SMT) solvers. The goals of SMT-COMP are to spur solver advances,
> >collect benchmarks, and encourage adoption of the SMT-LIB standard,
> >through friendly competition.
> >
> >SMT-COMP'18 will end in time to be described and the results announced
> >at the SMT Workshop (July 12-13), which is affiliated with the
> >International Joint Conference on Automated Reasoning (IJCAR 2018),
> >part of the Federated Logic Conference (FLoC 2018).
> >
> >SMT-COMP'18 is organized under the direction of the SMT Steering
> >committee. The organizing team for SMT-COMP'18 is
> >
> >    . Matthias Heizmann - University of Freiburg, Germany
> >    . Aina Niemetz      - Stanford University, USA
> >    . Giles Reger       - University of Manchester, UK
> >    . Tjark Weber       - Uppsala University, Sweden
> >
> >This is a call for three things:
> >
> >
> >CALL FOR COMMENTS:
> >
> >The organizing team is preparing the schedule and rules for 2018. Any
> >comments you may have to improve the competition over past years or to
> >redirect its focus are welcome and will be considered by the team. We
> >particularly appreciate comments received until April 8, 2018.
> >
> >For SMT-COMP'18, we are especially interested in comments regarding:
> >
> >- Certificates, trophies, awards: Past competitions have been
> >  somewhat unceremonious. What would be good ways to increase
> >  ceremony and recognition for winning solvers? How should
> >  trophies or other prizes be funded?
> >
> >- Scope: New SMT-LIB theories for strings and for reals with
> >  transcendental functions are currently in preparation. Are
> >  corresponding benchmarks and sufficiently stable solver
> >  implementations available for SMT-COMP to feature these as
> >  (experimental) divisions in 2018? Should the scope or emphasis
> >  of the competition be adapted in other ways?
> >
> >
> >CALL FOR BENCHMARKS:
> >
> >The competition is enhanced by new sets of benchmarks to add to those
> >already in use (and used in past competitions). A selection of
> >benchmarks in various categories is used for the competition.
> >
> >If you have benchmarks that you think would be useful to SMT-LIB and
> >SMT-COMP (and may be made public), please let us know as soon as
> >possible, even if the material is not quite ready. We will work in
> >close cooperation with the SMT-LIB maintainers to integrate such
> >benchmarks into the SMT-LIB. The deadline for submission of new
> >benchmarks to be used in the 2018 competition is
> >
> >    *** April 8, 2018. ***
> >
> >
> >PRELIMINARY CALL FOR SOLVERS:
> >
> >A submission deadline for solvers will be announced along with the
> >rules. However, it is useful to the organizing team to know in advance
> >which and how many solvers may be entering. If you have not submitted
> >a solver before, or if you think there may be unusual circumstances,
> >we request that you let us know at your earliest convenience if you
> >think you may be submitting one or more solvers to SMT-COMP'18.
> >
> >
> >COMMUNICATION:
> >
> >The competition website will be at www.smtcomp.org.
> >
> >Public email regarding the competition may be sent to
> >smt-comp at cs.nyu.edu.
> >
> >Announcements will be sent to both smt-comp at cs.nyu.edu and
> >smt-announce at googlegroups.com.
> >
> >Non-confidential email to the organizers may be sent to
> >smtcomp-discussion at lists.sourceforge.net.
> >
> >Sincerely,
> >The organizing team
> >
> >
> >_______________________________________________
> >SMT-COMP mailing list
> >SMT-COMP at cs.nyu.edu
> >https://cs.nyu.edu/mailman/listinfo/smt-comp
>
> --
> Paulo Matos
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/smt-comp
>