CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses

TL;DR

CHCVERIF is a portfolio-based solver that leverages existing software verification tools to solve Constrained Horn Clauses, showing promising results especially on bitvector benchmarks and highlighting the potential of this approach.

Contribution

This paper introduces CHCVERIF, a novel portfolio-based CHC solver that reuses mature software verification tools, expanding the toolkit for solving CHCs in verification tasks.

Findings

Moderate success with linear integer arithmetic

Modest success on bitvector benchmarks

Demonstrates viability of software verification tools as CHC backends

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.