Competition Report: CHC-COMP-20

TL;DR

CHC-COMP-20 is a competition evaluating nine solvers for Constrained Horn Clauses across multiple tracks involving linear integer and real arithmetic and arrays, providing insights into solver performance.

Contribution

This report details the design, organization, and results of the third CHC-COMP solver competition, highlighting advancements in solver evaluation for various logical theories.

Findings

Nine solvers participated in four tracks.

Evaluation conducted on problems in linear integer and real arithmetic, and arrays.

Results provide benchmarks for solver performance and progress.

Abstract

CHC-COMP-20 is the third competition of solvers for Constrained Horn Clauses. In this year, 9 solvers participated at the competition, and were evaluated in four separate tracks on problems in linear integer arithmetic, linear real arithmetic, and arrays. The competition was run in the first week of May 2020 using the StarExec computing cluster. This report gives an overview of the competition design, explains the organisation of the competition, and presents the competition results.