2020 | Format | 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 of the second CHC-COMP will be announced at the HCVS workshop affiliated with ETAPS 2020.

UPDATE March 20

Due to the Corona virus situation, ETAPS 2020 and the HCVS workshop have been postponed, and it is not clear when either event will take place. We are planning to run the competition still mostly as planned, and announce the competition results on this webpage, as well as in a short competition report published together with the HCVS proceedings (likely before the actual HCVS workshop).

Participants (Tool, Submitter)

The list of participants will be made public, together with the competition results, at the HCVS workshop (April 26). If you would like to submit a solver, and have not yet been in touch with the organisers, please add a note in the Gitter chat, or send a mail to Philipp Ruemmer.

Benchmarks

The competition benchmarks will be selected among the benchmarks available on Github. If you have benchmarks of any kind that can be made public, and that are not yet on Github, please upload! The final list of benchmarks used in the competition will be made public, together with the competition results, on April 26.

The following tracks will be evaluated at CHC-COMP 2020 (no change compared to 2019):

   LIA-Lin:    Linear Integer Arithmetic, linear clauses
   LIA-Nonlin:    Linear Integer Arithmetic, nonlinear clauses
   LIA-Lin-Arrays:    Linear Integer Arithmetic + arrays, linear clauses
   LRA-TS:    Linear Real Arithmetic, transition systems
(exactly one uninterpreted relation symbol, three clauses)

Important Dates for 2020

   Submission deadline for benchmarks considered for the competition:    March 31 2020   April 15 2020
   Solver submission deadline for test runs:    March 31 2020   April 15 2020
   Final solver submission deadline for evaluation:    April 15 2020   April 30 2020
   Presentation of results:    April 26 2020 (HCVS workshop)   tba

Organizers

Big thanks to

Previous editions of CHC-COMP


Last updated: 2020-03-23 20:52:31 +0000