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

[Carsten F. <ca...@dc...>]

Dear SMT-COMP'18 organisers,

First of all, many thanks for running the competition! Tool competitions
like this (and the I/O format standardisation that they necessitate)
really make the corresponding research and tools more accessible to
external users.

I have a comment on the following:

> - 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?

Even awarding certificates that are printed on paper (at negligible
cost) may be beneficial. Imagine that you are a postdoc developing an
SMT solver, and you are preparing a job talk for an academic position.
In that situation, it can be very handy if you have a visual way to
communicate your achievements, say via a slide with an official
certificate stating that your SMT solver scored highest at the recent
SMT-COMP.

The academics in the audience (who come from backgrounds all over
computer science) may have no idea of what this strange "SMT" thing is,
but they will recognise an award from a tool competition when they see
one ... This may actually also benefit the SMT community as a whole.

As far as I recall, such certificates were handed out to category
winners at SMT-COMP 2014, when SMT-COMP was part of the FLoC Olympic
Games 2014. I think that this was a great idea, and I would like to
encourage doing so also at SMT-COMP 2018!

(This suggestion is independent from having further ceremony e.g. at the
SMT workshop, where such awards could be handed over to the authors of
the winning tools.)

Best regards,

  Carsten

On 16.03.2018 16:30, Tjark Weber 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...@cs....
> 
> Announcements will be sent to both smt...@cs... and
> smt...@go....
> 
> Non-confidential email to the organizers may be sent to
> smt...@li....
> 
> Sincerely,
> The organizing team
> 
> 
> _______________________________________________
> SMT-COMP mailing list
> SMT...@cs...
> https://cs.nyu.edu/mailman/listinfo/smt-comp
> 

-- 
Carsten Fuhs
Birkbeck, University of London
Department of Computer Science and Information Systems
http://www.dcs.bbk.ac.uk/~carsten/