2023 | HCVS | TOOLympics | 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 sixth CHC-COMP will be announced at the HCVS workshop affiliated with ETAPS 2023. CHC-COMP 2023 will also be part of TOOLympics 2023 at ETAPS 2023. |
Competition Results
- Presentation of the results at HCVS on April 23
- Competition Report (To appear in EPTCS)
Participants (Tool, Submitter)
The list of participants will be made public, together with the competition results, at the HCVS workshop (April 23). 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 and
Solver Submission
Solvers have to be provided in the form of a StarExec package (information about how to configure and upload a solver can be found in the StarExec user guide). As an example, you can have a look at the Eldarica package from 2019. Test your solver on StarExec before submitting! Submission is done by sending a link or the package to and
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, on April 23.
The following tracks will be evaluated at CHC-COMP 2023:
| 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 |
In addition to the theories listed in the track names, benchmarks can also use the Bool theory.
Important Dates for 2023
| Submission deadline for benchmarks considered for the competition: | March 24 2023 | ||
| Solver submission deadline for test runs (optional, but recommended): | March 31 2023 | ||
| Final solver submission deadline for evaluation: | April 7 2023 | ||
| Presentation of results: | April 23 2023 (HCVS workshop), and | ||
| April 26 2023 (TOOLympics session) |
Solvers Evaluation & Ranking
The description of the evaluation process and the ranking method of solvers is described in CHC-COMP 2022: Competition Report.
Organizers
Emanuele De Angelis, Inst. for Systems Analysis and Computer Science "A. Ruberti" - National Research Council, Italy
Hari Govind V K, University of Waterloo, Canada
Big thanks to
- Everybody who organized and helped with
the competition infrastructure over the last years:
Nikolaj Bjørner, Adrien Champion, Grigory Fedyukovich, Arie Gurfinkel, Dejan Jovanovic, and Philipp Ruemmer - Aaron Stump and StarExec!
Previous editions of CHC-COMP
Last updated: 2024-04-08 13:22:59 +0000