Constrained Horn Clauses (CHCs) are widely adopted as intermediate representations for a variety of verification tasks, including safety checking, invariant synthesis, and interprocedural analysis. This paper introduces CHCVERIF, a portfolio-based CHC solver that adopts a software verification approach for solving CHCs. This approach enables us to reuse mature software verification tools to tackle CHC benchmarks, particularly those involving bitvectors and low-level semantics. Our evaluation shows that while the method enjoys only moderate success with linear integer arithmetic, it achieves modest success on bitvector benchmarks. Moreover, our results demonstrate the viability and potential of using software verification tools as backends for CHC solving, particularly when supported by a carefully constructed portfolio.

翻译：约束霍恩子句（CHCs）被广泛用作多种验证任务（包括安全性检查、不变量综合和过程间分析）的中间表示。本文介绍了CHCVERIF，一种基于组合策略的CHC求解器，它采用软件验证方法来解决CHCs。该方法使我们能够复用成熟的软件验证工具来处理CHC基准测试，特别是涉及位向量和底层语义的测试。我们的评估表明，虽然该方法在线性整数算术上仅取得中等程度的成功，但在位向量基准测试中取得了较为可观的成果。此外，我们的结果证明了将软件验证工具作为CHC求解后端（尤其是在精心构建的组合策略支持下）的可行性和潜力。