SMT-COMP 2024: Final Call for Solvers
Martin Bromberger
================================================
18th International Satisfiability Modulo Theories Competition
(SMT-COMP'24)
FINAL CALL FOR SOLVERS
=================================================
We now invite registration of solvers for SMT-COMP 2024.
Solvers are entered into the competition via a push request to the SMT-COMP GitHub repository at
https://github.com/SMT-COMP/smt-comp.github.io/tree/master/submissions.
Detailed instructions can be found in the README file there. Note that solvers must be uploaded to a publicly available space as a docker file that compiles the solver and the final version must be a Zenodo (https://zenodo.org/) submission for reproducibility.
The submission deadline for (first versions of) solvers is
***May 27, 2024. ***
After the above date, no new entrants will be accepted. However,
submitted solvers may be updated via a push request until
***June 8, 2024. ***
We plan to publish the results including all materials in an artifact.
By participating, you agree that we may copy your solver binaries to
this artifact. Please include a license file of your choice with your
solver binaries. Please contact us, if you want to include other files
with the artifact.
Note that a short system description of 1-2 pages (see Section 4 of the
competition rules at https://smt-comp.github.io/2024/rules.pdf) is part
of the solver submission and MANDATORY. Submission of the system
description is THIS YEAR due for the initial solver deadline on May 27,
2024. Participants are asked to provide a link to the system
description in the registration form. The system description can be
updated until June 8, 2024, however it must be reviewable by the
initial solver deadline. The links to the final solver submission must be
provided via a push request to the organizers by the final deadline.
The single query, incremental, unsat-core, and model-validation tracks
will no longer run on StarExec (http://www.starexec.org) because
StarExec is in the process of being decommissioned. Starting this year,
we will run these tracks on the BenchExec cluster
(https://github.com/sosy-lab/benchexec) owned by LMU's Software and
Computational Systems Lab (SoSy-Lab https://www.sosy-lab.org/), who
are kind enough to support our competition with their computing power.
To be more precise, the competition will be run on the 168 apollon nodes
of the SoSy-Lab BenchExec cluster (for more details see
https://vcloud.sosy-lab.org/cpachecker/webclient/master/info).
It is also possible to locally emulate and test the computing environment
on the competition machines using the following instructions:
You can use last year’s pre-/post-processors for testing. Note that for
testing your solver in the incremental track you need to wrap the trace
executor around your solver, see
https://github.com/smt-comp/trace-executor#wrapping-your-solver.
If you don’t wrap it yourself, we will wrap your solver in the competition.
Your solver can have multiple configurations for different tracks, logics, etc.
These can be specified as part of the solver submission and changed
until the deadline for the final solver. The default configuration is used for
all other tracks.
As in the last year, we organize a separate parallel and cloud solving
track, hosted by Amazon Web Services. For more information on the
participation on these two tracks, see
https://smt-comp.github.io/2024/parallel-and-cloud-tracks.html.
Finally, we have decided to discontinue the proof exhibition track.
There are three reasons that led to this decision. First, we were
unable to find a way of turning the proof track into an actual competition
that would not lead to an unmanageable amount of overhead on the
competition organizers or the participants. Second, we have collected
vast amounts of data in the last two years and thoroughly evaluating it
takes time. Third, this year we would need to severely restrict the
allowed proof size due to hardware limits of the new execution platform.
Please see the competition rules for further details.
Sincerely,
The organizing team
Martin Bromberger (chair), MPI for Informatics, Germany
François Bobot, CEA List, France
Martin Jonáš, Masaryk University, Czech Republic