Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Multiple Query Satisfiability of Constrained Horn Clauses

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

TL;DR

The paper tackles satisfiability checking for sets of constrained Horn clauses (CHCs) that include multiple queries by introducing a transformation ${\mathcal{T}}_{\mathit{mq}}$ that yields an equisatisfiable CHC program in which inter-query dependencies are encoded and exploitable by solvers. Grounded in generalized catamorphisms for algebraic data types, the method constructs new definitions that fuse program predicates with catamorphism constraints, enabling mutual reasoning across queries. The authors prove soundness and completeness of the transformation, show termination for catamorphism-based queries, and demonstrate substantial practical gains: a benchmark of CHCs encoding ADT-manipulating programs is solved more effectively than by a state-of-the-art solver alone. The approach extends prior contracts-based transformations and Artefacts VeriCaT, providing a robust tool for verifying properties across multiple related verifications. Overall, ${\mathcal{T}}_{\mathit{mq}}$ enhances CHC-based verification by compiling query interactions into the CHC set, improving satisfiability proving for complex, multi-query verification problems.

Abstract

We address the problem of checking the satisfiability of a set of constrained Horn clauses (CHCs) possibly including more than one query. We propose a transformation technique that takes as input a set of CHCs, including a set of queries, and returns as output a new set of CHCs, such that the transformed CHCs are satisfiable if and only if so are the original ones, and the transformed CHCs incorporate in each new query suitable information coming from the other ones so that the CHC satisfiability algorithm is able to exploit the relationships among all queries. We show that our proposed technique is effective on a non trivial benchmark of sets of CHCs that encode many verification problems for programs manipulating algebraic data types such as lists and trees.

Multiple Query Satisfiability of Constrained Horn Clauses

TL;DR

The paper tackles satisfiability checking for sets of constrained Horn clauses (CHCs) that include multiple queries by introducing a transformation that yields an equisatisfiable CHC program in which inter-query dependencies are encoded and exploitable by solvers. Grounded in generalized catamorphisms for algebraic data types, the method constructs new definitions that fuse program predicates with catamorphism constraints, enabling mutual reasoning across queries. The authors prove soundness and completeness of the transformation, show termination for catamorphism-based queries, and demonstrate substantial practical gains: a benchmark of CHCs encoding ADT-manipulating programs is solved more effectively than by a state-of-the-art solver alone. The approach extends prior contracts-based transformations and Artefacts VeriCaT, providing a robust tool for verifying properties across multiple related verifications. Overall, enhances CHC-based verification by compiling query interactions into the CHC set, improving satisfiability proving for complex, multi-query verification problems.

Abstract

We address the problem of checking the satisfiability of a set of constrained Horn clauses (CHCs) possibly including more than one query. We propose a transformation technique that takes as input a set of CHCs, including a set of queries, and returns as output a new set of CHCs, such that the transformed CHCs are satisfiable if and only if so are the original ones, and the transformed CHCs incorporate in each new query suitable information coming from the other ones so that the CHC satisfiability algorithm is able to exploit the relationships among all queries. We show that our proposed technique is effective on a non trivial benchmark of sets of CHCs that encode many verification problems for programs manipulating algebraic data types such as lists and trees.
Paper Structure (8 sections, 3 theorems, 3 equations, 5 figures, 1 table)

This paper contains 8 sections, 3 theorems, 3 equations, 5 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminary Notions
  3. An Introductory Example
  4. Catamorphism-based Queries
  5. Transformation Rules
  6. Transformation Algorithm
  7. Experimental Evaluation
  8. Conclusions and Related Work

Key Result

theorem 1

Let $S_0 \Mapsto S_1 \Mapsto \ldots \Mapsto S_n$ be a transformation sequence using rules R1--R4. Then, $S_0$ is satisfiable if and only if $S_n$ is satisfiable.

Figures (5)

  • Figure 1: (A) Generalized list catamorphism. (B) Generalized tree catamorphism.
  • Figure 2: Program clauses for Insertion Sort.
  • Figure 3: Property clauses for Insertion Sort: (A) the catamorphisms.
  • Figure 4: Property clauses for Insertion Sort: (B) the queries.
  • Figure 5: The $\mathit{Define}$, $\mathit{Unfold}$, $\mathit{Strengthen}$, and $\mathit{Fold}$ functions.

Theorems & Definitions (8)

  • definition 1: Generalized Catamorphisms
  • definition 2
  • definition 3: One-step Unfolding
  • theorem 1: Soundness and Completeness of the Rules
  • definition 4
  • definition 5
  • theorem 2: Termination of Algorithm ${\mathcal{T}}_{\mathit{mq}}$
  • theorem 3: Soundness and Completeness of Algorithm ${\mathcal{T}}_{\mathit{mq}}$