[SMT-COMP] SMT-COMP 2024: Preliminary Call for Solvers

[Martin Bromberger]

Hello everybody,


The submission deadline for the first version of the solvers is on May 
27. However, it is useful for 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, 
please let us know at your earliest convenience if you think you may be 
submitting a solver to SMT-COMP'24. We require a system description for 
all submitted solvers as part of the submission of the preliminary 
solver versions (deadline May 27).


The single query, incremental, unsat-core, model-validation and proof 
exhibition 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 trackson the 
BenchExec cluster (https://github.com/sosy-lab/benchexec 
<https://github.com/sosy-lab/benchexec>) owned by LMU's Software and 
Computational Systems Lab (SoSy-Lab https://www.sosy-lab.org/ 
<https://www.sosy-lab.org/>), who are kind enough to support our 
competition with their computing power.


Participants are now required to upload their final solver versions as a 
Zenodo (https://zenodo.org/ <https://zenodo.org/>) submission that must 
contain a docker file that compiles the solver. Moreover, we will change 
our submission process from a google form to a push request to the 
SMT-COMP GitHub repository 
(https://github.com/SMT-COMP/smt-comp.github.io/tree/master/submissions 
<https://github.com/SMT-COMP/smt-comp.github.io/tree/master/submissions>). 
Detailed instructions can be found in the README file there.


The parallel and cloud tracks will again run on AWS, which is kindly 
supporting them. Participants of these tracks are required to submit 
their solver via a GitHub repository (which can be private). The 
repository should contain a docker file that compiles the solver. 
Detailed instructions for submitting to these tracks are available here 
(they lift to SMT):


https://github.com/aws-samples/aws-batch-comp-infrastructure-sample 
<https://github.com/aws-samples/aws-batch-comp-infrastructure-sample>


To participate teams must emailaws-smtcomp-2024 at googlegroups.com 
<https://groups.google.com/>with the following:


1. name of the solver and a list of the authors

2. your AWS account number

3. the URL of the GitHub repository including the branch

4. the full, 40-character SHA-1 hash of the commit


There are also some potential changes that we are considering for future 
editions of the competition (so for SMT-COMP 2025 and onwards). These 
changes would make our lives much easier (= reduce complexity of our 
scripts and the manual preprocessing from our side), but might cause 
issues for you. Therefore, we would like to know if any of the following 
potential changes would cause serious issues for you and why:

 1.

    The preliminary versions of the solvers (and not just the final
    versions) must be available on zenodo

 2.

    Each team may only submit one archive or, to be more precise,
    different archives by the same team will be treated as separate
    submissions/solvers

 3.

    Scripts for command-line options are no longer allowed, i.e., the
    solvers should be able to analyze the problems and adjust their
    settings internally with just the name of the track.

 4.

    Each submission may only have one string of command-line options and
    not separate strings of options for the different divisions/tracks
    they participate in

The last three changes would have the additional benefit that for users 
of our tools it becomes much more transparent how to reproduce the 
competition results without the knowledge where to find the competition 
scripts/options or that such scripts/options exist at all.


Best,


The organizing team

Martin Bromberger (chair), MPI for Informatics, Germany

François Bobot, CEA List, France

Martin Jonáš, Masaryk University, Czech Republic
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5772 bytes
Desc: Kryptografische S/MIME-Signatur
URL: </pipermail/smt-comp/attachments/20240219/bafc36a7/attachment-0001.p7s>