Call for Participation | Organizers | Tracks | Dates | Rules | HCVS | Github | Gitter

Constrained Horn Clauses (CHC) is a fragment of First
Order Logic (FOL) that is sufficiently expressive to
describe many verification, inference, and synthesis
problems including inductive invariant inference, model
checking of safety properties, inference of procedure
summaries, regression verification, and sequential
equivalence. The CHC competition (CHC-COMP) will compare
state-of-the-art tools for CHC solving with respect to
performance and effectiveness on a set of publicly
available benchmarks. The winners among participating
solvers are recognized by measuring the number of
correctly solved benchmarks as well as the runtime. The
results will be announced in the HCVS workshop
affiliated with CAV,
ICLP
and IJCAR at FLoC 2018. |

**Tracks**:

Linear CHC over LRA

Linear CHC over LIA

Linear CHC over LIA + Array

**Important Dates**:

Mar 15: First draft of the benchmarks is publicly available

Jun 1: Initial deadline for submitting solvers

Jul 13: Announcement of results at HCVS

**Rules and competition procedure**:

Benchmarks will use (a subset of) version 2.6 of the SMT-LIB language.

The result of a solving run is a tuple <

**sat**|**unsat**|**unknown**,**TIME**>:**sat**when the system is satisfiable. That is, there exist an interpretation of all uninterpreted relation symbols in the system making all clauses valid**unsat**when the system is unsatisfiable**unknown**when a solver failed to find a solution and has given up**TIME**is the consumed CPU time in seconds until the solver converges.

If the run exceeds the predefined timeout (15 min) the result is interpreted as unknown.

There is no requirement on a witness generation (neither for models (sat) nor refutations (unsat)).

The total score for each solver is calculated by the formula:

**S_correct - 2 * S_incorrect**, where**S_correct**(resp.**S_incorrect**) is the number of correctly (resp. incorrectly) solved benchmarks.All participating solvers should be submitted by its authors to the StarExec platform.

Each submitted solver must have one configuration only. The authors are responsible of any technical problems while running the configuration on StarExec.

All participants are encouraged (but not required) to provide a short (1–2 pages) description of the solver and give a short (5 min) talk at the workshop.

**Organizers**:

Arie Gurfinkel, University of Waterloo, Canada

Philipp Ruemmer, Uppsala University, Sweden

Grigory Fedyukovich, Princeton University, USA

Adrien Champion, University of Tokyo, Japan

*Last updated: 2018-04-15 13:51:13 +0000 *