[SMT-COMP] SMT-COMP 2018: Call for Comments, Benchmarks, Solvers
Tjark Weber
tjark.weber at it.uu.se
Fri Mar 16 12:30:02 EDT 2018
======================================================================
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
More information about the SMT-COMP
mailing list