|
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 third CHC-COMP will be announced at the HCVS workshop
affiliated with ETAPS 2020. |
Competition Results
- Report (announced May 19 2020, final version from June 11 2020)
- Summary for LIA-Lin
- Summary for LIA-Nonlin
- Summary for LIA-Lin-Arrays
- Summary for LRA-TS
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).
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: |
|
||
| Solver submission deadline for test runs: |
|
||
| Final solver submission deadline for evaluation: |
|
||
| Presentation of results: |
|
Organizer
Philipp Ruemmer, Uppsala University, Sweden
Big thanks to
- Everybody who helped with the competition infrastructure over the last years:
Arie Gurfinkel, Grigory Fedyukovich, Adrien Champion, Dejan Jovanovic, Nikolaj Bjørner, and others. - StarExec!
Previous editions of CHC-COMP
Last updated: 2024-04-08 13:22:59 +0000