核心概念
The CHC-COMP 2023 competition evaluated state-of-the-art solvers for Constrained Horn Clauses, a formalism widely used in program verification. The competition featured seven solvers and six tracks, each focusing on a class of CHCs with different background theories and constraints.
摘要
The CHC-COMP 2023 was the sixth edition of the annual competition for Constrained Horn Clause (CHC) solvers. The competition featured seven solvers, six of which were competing and one was entered as hors concours. The competition was organized into six tracks, each dealing with a class of CHCs with different background theories and constraints:
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 - nonlinear 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
The competition was run on the StarExec platform, with each solver given a time limit of 1800 seconds for the competition runs. The results were evaluated based on the number of satisfiable and unsatisfiable benchmarks solved by each solver in each track. In case of a tie, the total CPU time was used to determine the ranking.
The winners of the competition were:
LIA-lin: Golem
LIA-nonlin, LIA-lin-Arrays, LIA-nonlin-Arrays, LIA-nonlin-Arrays-nonrecADT, ADT-LIA-nonlin: Eldarica
The report also discusses some issues encountered during the competition runs and how they were resolved in collaboration with the participants. Finally, it outlines some open issues and proposals for future editions of the competition.