Competition of Solvers for Constrained Horn Clauses (CHC-COMP 2023)

Constrained Horn Clauses (CHC) are a fragment of first-order logic that is expressive enough to represent many important software verification tasks, yet practical for fully automatic techniques. CHCs are used to verify the safety of hardware, software, and hybrid systems, infer refinement types, analyse program termination, and prove the correctness of smart contracts, among other applications. Over the years, many researchers have developed a variety of tools to check the satisfiability of CHCs. CHC-COMP strives to bring together these research efforts and compare the effectiveness of different CHC solvers on a unified set of benchmarks. Each year, CHC-COMP collects benchmarks provided by the CHC community, organizes them into tracks, and evaluates CHC solvers against those tracks. This annual competition is now in its sixth year. This report gives an overview of CHC-COMP and details of its sixth edition.