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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

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

  • Emanuele De Angelis,
  • Hari Govind Vediramana Krishnan

摘要

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.