2018 | 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 will be announced in the HCVS workshop affiliated with CAV, ICLP and IJCAR at FLoC 2018.


Participants (Tool, Submitter)

Benchmarks

Results

Organizers


Last updated: 2024-04-08 13:22:59 +0000