Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Catamorphic Abstractions for Constrained Horn Clause Satisfiability

Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti

TL;DR

The paper tackles satisfiability checking for CHCs that encode properties via catamorphisms on algebraic data types. It introduces a transformation ${\mathcal{T}}_{abs}$ that unfolds, adds catamorphisms, folds, and erases to produce equisatisfiable CHCs free of catamorphisms, by computing a least fixpoint $\tau_{fix}$ on a finite lattice. Implemented as VeriCaT_abs on VeriMAP and evaluated with Z3/SPACER and Eldarica, it demonstrates strong improvements in proving sat properties (e.g., $109/114$ after transformation) while maintaining solid unsat performance, validating a practical two-step verification approach. The work situates itself within abstract interpretation and offers a robust alternative to solver extensions for ADTs, with potential for extension to other theories and automatic catamorphism selection.

Abstract

Catamorphisms are functions that are recursively defined on list and trees and, in general, on Algebraic Data Types (ADTs), and are often used to compute suitable abstractions of programs that manipulate ADTs. Examples of catamorphisms include functions that compute size of lists, orderedness of lists, and height of trees. It is well known that program properties specified through catamorphisms can be proved by showing the satisfiability of suitable sets of Constrained Horn Clauses (CHCs). We address the problem of checking the satisfiability of those sets of CHCs, and we propose a method for transforming sets of CHCs into equisatisfiable sets where catamorphisms are no longer present. As a consequence, clauses with catamorphisms can be handled without extending the satisfiability algorithms used by existing CHC solvers. Through an experimental evaluation on a non-trivial benchmark consisting of many list and tree processing algorithms expressed as sets of CHCs, we show that our technique is indeed effective and significantly enhances the performance of state-of-the-art CHC solvers.

Catamorphic Abstractions for Constrained Horn Clause Satisfiability

TL;DR

The paper tackles satisfiability checking for CHCs that encode properties via catamorphisms on algebraic data types. It introduces a transformation that unfolds, adds catamorphisms, folds, and erases to produce equisatisfiable CHCs free of catamorphisms, by computing a least fixpoint on a finite lattice. Implemented as VeriCaT_abs on VeriMAP and evaluated with Z3/SPACER and Eldarica, it demonstrates strong improvements in proving sat properties (e.g., after transformation) while maintaining solid unsat performance, validating a practical two-step verification approach. The work situates itself within abstract interpretation and offers a robust alternative to solver extensions for ADTs, with potential for extension to other theories and automatic catamorphism selection.

Abstract

Catamorphisms are functions that are recursively defined on list and trees and, in general, on Algebraic Data Types (ADTs), and are often used to compute suitable abstractions of programs that manipulate ADTs. Examples of catamorphisms include functions that compute size of lists, orderedness of lists, and height of trees. It is well known that program properties specified through catamorphisms can be proved by showing the satisfiability of suitable sets of Constrained Horn Clauses (CHCs). We address the problem of checking the satisfiability of those sets of CHCs, and we propose a method for transforming sets of CHCs into equisatisfiable sets where catamorphisms are no longer present. As a consequence, clauses with catamorphisms can be handled without extending the satisfiability algorithms used by existing CHC solvers. Through an experimental evaluation on a non-trivial benchmark consisting of many list and tree processing algorithms expressed as sets of CHCs, we show that our technique is indeed effective and significantly enhances the performance of state-of-the-art CHC solvers.
Paper Structure (2 sections, 2 theorems, 1 table)

This paper contains 2 sections, 2 theorems, 1 table.

Table of Contents

  1. Implementation and Experimental Evaluation
  2. Conclusions and Related Work

Key Result

Lemma 1

The operator $\tau_{P\cup\{Q\},\alpha}$ is monotonic on the finite lattice $\mathcal{P}_m(\mathcal{D})$. Thus, it has a least fixpoint $\textit{lfp}(\tau_{P\cup\{Q\},\alpha})$, also denoted $\tau_{\mathit{fix}}$, which is equal to $\tau_{P\cup\{Q\},\alpha}^n(\emptyset)$, for some natural number $n$.

Theorems & Definitions (5)

  • Definition 3: Domain of Definitions
  • Definition 4
  • Lemma 1: Existence and Uniqueness of the Fixpoint of $\tau_{P\cup\{Q\},\alpha}$
  • Theorem 3: Total Correctness of Algorithm ${\mathcal{T}}_{\space\mathit{abs}}$
  • Example 8