CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses

TL;DR

The paper addresses solving Constrained Horn Clauses (CHCs) by reusing mature software verifiers through a translation to C programs. It introduces CHCVerif, a portfolio-based CHC solver built on CoVeriTeam that orchestrates multiple verifiers for linear integer arithmetic and bitvector CHCs. The approach shows limited success for linear integer arithmetic due to semantic and overflow challenges but achieves modest success on bitvector benchmarks, highlighting the value of software verification backends for CHC solving. This translation-based strategy broadens CHC solver capabilities to low-level theories and points to future extensions, including floating-point support, to enhance applicability.

Abstract

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.

Figures (2)

• Figure 1: Overview of the proposed approach
• Figure 2: The proposed portfolio for the LIA theory