2025 | Format | Rules | Github |

CHC-COMP

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.

CHC-COMP is associated with the Workshop on Horn-Clause Verification and Synthesis HCVS 2025.

New: Mailing List

Please register here https://software.imdea.org/mailman3/postorius/lists/chc-comp.software.imdea.org to receive updates and to participate in the discussion

Note, there is also the ealier Gitter chatroom, but this seemed to have little popularity. Please be aware that we will not necessarily be responsive over there.

Organizers

Preliminary Schedule

  • April 10: participation registration soft deadline
  • April 10: benchmark submission hard deadline
  • April 17: solver submission deadline

Originally, the schedule aimed at presenting the results at ETAPS 2025. However, as HCVS 2025 has been announced at CAV 2025, we might relax the schedule to this event.

Solver submission

Participation guidelines will be published shortly and announced on the mailing list.

We will offer pre-runs on a subset of benchmarks for solvers until the soft registration deadline on April 10 to test that everything works properly.

Infrastructure

The key difference to earlier years will be that evaluations will run on the SV-COMP infrastructure at the LMU Munich.

  • You can already test your solver in the competition environment, which is provided as a Docker file. It is based on standard Ubuntu 24.04.
  • If you are missing a standard software package from the list provided there, you may consider submitting a pull requests, but we do not guarantee that this will be honored.
  • Please otherwise package all additional dependencies with your solver submission.
  • We aim to keep the overhead on the side of participants low. This means we will offer a standard way to integrate, similar to the one on StarExec. Typical SV-COMP participation steps, like submitting a toolinfo module or benchmark definitions are not necessary for CHC-COMP.
  • We will likely use this type of machine: Intel Xeon E3-1230 v5 @ 3.40 GHz, 4x2 cores with hyperthreading, 33GB of main memory. Results will be reported by wall-time and by CPU time to illustrate the benefits of solvers that can run parallel threads.

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 format of the benchmarks is described here; a detailed description of the benchmark selection process can be found in CHC-COMP 2022: Competition Report. The final list of benchmarks used in the competition will be made public, together with the competition results.

The following tracks are planned for CHC-COMP 2025

  • LIA-lin: Linear Integer Arithmetic, linear clauses
  • LIA-nonlin: Linear Integer Arithmetic, nonlinear clauses
  • LIA-lin-Arrays: Linear Integer Arithmetic + arrays, linear clauses
  • LIA-nonlin-Arrays: Linear Integer Arithmetic + arrays, non-linear clauses
  • LIA-nonlin-Arrays-nonrecADT: Linear Integer Arithmetic + arrays + non-recursive Algebraic data-types, nonlinear clauses
  • ADT-LIA-nonlin: Algebraic data-types + Linear Integer Arithmetic, nonlinear clauses
  • LRA: Linar Real Arithmetic (tentative)

In addition to the theories listed in the track names, benchmarks can also use the Bool theory.

Novel features of CHC-COMP in 2025

  • Model Validation: We introduce a model validation demo track. Participants can opt-in to have their sat models checked independently. We will report these results separately from the main standings. Details and format are being clarified at the moment.
  • Massively Parallel Track: We may run selected evaluations with on a machine with 256 cores. Please get in touch if you think your solver may be able to make use of this.

Big thanks to

  • Everybody who organized and helped with the competition infrastructure over the last years, notably:
    Nikolaj Bjørner, Adrien Champion, Emanuele De Angelis, Grigory Fedyukovich, Hari Govind V K, Arie Gurfinkel, Dejan Jovanovic, and Philipp Ruemmer

  • Aaron Stump and StarExec!

Previous Editions

Last updated: 2025-03-11 14:52:17 +0000