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

[Tjark Weber]

======================================================================

    10th International Satisfiability Modulo Theories Competition
                            (SMT-COMP'15)

                            July 19, 2015
                          San Francisco, USA

                          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'15 will end in time to be described and the results announced
at the SMT Workshop (July 18-19), which is affiliated with the 27th
International Conference on Computer Aided Verification (CAV 2015).

SMT-COMP'15 is organized under the direction of the SMT Steering
committee. The organizing team for SMT-COMP'15 is

    . Sylvain Conchon - Paris-Sud University, France
    . David Deharbe - Federal University of Rio Grande do Norte, Brazil
    . 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 2015.
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. Please submit such comments by *** 22 February 2015. ***

For SMT-COMP'15, we are particularly interested in comments regarding:

- Sequential vs. parallel performance: All solvers will have several
CPU cores available, and we plan to measure CPU and wall time. Solver
developers might wish to prepare both sequential and parallel versions
of their solvers.

- Benchmark selection: We will likely have sufficient computational
resources to run all solvers on all eligible benchmarks. Therefore, we
are interested in proposals for weighing the results so as to avoid
over-representation of certain (large) benchmark families.

- Scope: After the successful migration to StarExec in 2013/14, we are
considering to broaden the scope of SMT-COMP again. We might reinstate
additional tracks, e.g., for unsat core extraction and proof-producing
solvers.

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 (according
to rules that are currently being revised).

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 include such
benchmarks in the SMT-LIB in time to be taken into account for the
competition. The deadline for benchmarks to be used in the 2015
competition will be announced when the schedule and rules are
finalized.

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. Thus 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'15, particularly if you
think there may be unusual circumstances.

COMMUNICATION:

The competition web-site 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 on both smt-comp at cs.nyu.edu and
smt-lib at cs.nyu.edu.

Email to the organizers only may be sent to
smtcomp-discussion at lists.sourceforge.net

Sincerely,
The organizing team