[SMT-COMP] Request for Comments: 1st International Constrained Horn Clause Satisfiability Competition (CHC-COMP'18)

Alberto Griggio griggio at fbk.eu
Wed Mar 7 08:48:40 EST 2018


================================================================================
1st International Constrained Horn Clause Satisfiability Competition
                            (CHC-COMP'18)
        https://chc-comp.github.io/2018/call-for-comments.html

                            July 13, 2018
                        Oxford, United Kingdom

                          CALL FOR COMMENTS
                         CALL FOR BENCHMARKS
                     PRELIMINARY CALL FOR SOLVERS
================================================================================

CHC-COMP is the annual competition among Constrained Horn Clause
solvers. The goal of the competition is to advance development of
solvers, facilitate standardization and evolution of the input format,
collect benchmarks, and promote a friendly competition.

CHC-COMP'18 will end in time to be described and the results announced
during the HCVS Workshop (July 13), which is affiliated with the
International Conference on Computer Aided Verification (CAV 2018),
International Conference on Logic Programming (ICLP 2018) and
International Joint Conference on Automated Reasoning (IJCAR 2018) at
International Federated Logic Conference (FLoC 2018).

The organizers for CHC-COMP'18 are:

    - Arie Gurfinkel            University of Waterloo, Canada
    - Philipp Ruemmer           Uppsala University, Sweden
    - Grigory Fedyukovich       Princeton University, USA
    - Adrien Champion           University of Tokyo, Japan

This is a call for three things:

# CALL FOR COMMENTS:

The organizers are preparing the schedule and the rules for 2018.  Any
comments that you might have based on related competitions (SAT, SMT,
SVCOMP, etc.) to improve any aspect of the competition or improve the
focus of the competition will be considered by the organizers. We
particularly appreciate comments received by

             ** April 2, 2018 **

For CHC-COMP'18, we are particularly interested in comments regarding
the rules and the benchmark format that might prevent a potential
competitor from participating (e.g., complexities of the input format,
supported theories, considered CHC fragment, etc.)

# CALL FOR BENCHMARKS:

The competition crucially depends on a continuously renewed set of
benchmarks. A selection of benchmarks will be used for the
competition, in accordance with the rules that are currently being
discussed.

A preliminary collection of benchmarks can be found at
https://github.com/chc-comp. If you have benchmarks that can be made
publicly available and might be of interest to the competition, please
let us know; we are also interested in benchmarks that are not quite
ready, for example, because they are in a custom format. We will work
closely with any benchmark submitter to prepare the benchmarks for
inclusion in the current (or future) versions of CHC-COMP.

The deadline for the benchmarks to be used in the competition will be
announced together with the rules for the competition and benchmark
format.

# PRELIMINARY CALL FOR SOLVERS

A submission deadline for solvers will be announced along with the
rules. However, it is useful for us to know in advance the potential
number of participants. If you plan or consider to participate, please
let us know as soon as possible. In particular, let us know if there
are changes to the rules and to the format that might block your
participation.

This can be done by participating in the following poll

https://doodle.com/poll/gdk2vy5euvfcc67v


# COMMUNICATION

The competition web-site is https://chc-comp.github.io.

Announcements and discussions on gitter at https://gitter.im/chc-comp.

The competition GitHub organization is https://github.com/chc-comp.

-- 
--
Le informazioni contenute nella presente comunicazione sono di natura privata 
e come tali sono da considerarsi riservate ed indirizzate esclusivamente ai 
destinatari indicati e per le finalità strettamente legate al relativo 
contenuto. Se avete ricevuto questo messaggio per errore, vi preghiamo di 
eliminarlo e di inviare una comunicazione all’indirizzo e-mail del mittente.
--
The information transmitted is intended only for the person or entity to 
which it is addressed and may contain confidential and/or privileged 
material. If you received this in error, please contact the sender and 
delete the material.


More information about the SMT-COMP mailing list