Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Theta as a Horn Solver

Levente Bajczi, Milán Mondok, Vince Molnár

TL;DR

Theta tackles verification of Constrained Horn Clauses by transforming CHCs into control-flow automata and applying a modular, portfolio-driven verification pipeline. The paper details the CHC-to-CFA transformation, CEGAR-based abstraction with two abstract domains, and a suite of bounded and diagram-based techniques that are integrated via a sequential portfolio. It also discusses model generation, software architecture, and a corrected re-evaluation on CHC-COMP benchmarks, highlighting improvements after fixing a misconfiguration. The findings demonstrate Theta’s competitive performance on linear CHCs and emphasize the value of modular design for scalable CHC solving in practice.

Abstract

Theta is a verification framework that has participated in the CHC-COMP competition since 2023. While its core approach -- based on transforming constrained Horn clauses (CHCs) into control-flow automata (CFAs) for analysis -- has remained mostly unchanged, Theta's verification techniques, design trade-offs, and limitations have remained mostly unexplored in the context of CHCs. This paper fills that gap: we provide a detailed description of the algorithms employed by Theta, highlighting the unique features that distinguish it from other CHC solvers. We also analyze the strengths and weaknesses of the tool in the context of CHC-COMP benchmarks. Notably, in the 2025 edition of the competition, Theta's performance was impacted by a configuration issue, leading to suboptimal results. To provide a clearer picture of Theta's actual capabilities, we re-execute the tool on the competition benchmarks under corrected settings and report on the resulting performance.

Theta as a Horn Solver

TL;DR

Theta tackles verification of Constrained Horn Clauses by transforming CHCs into control-flow automata and applying a modular, portfolio-driven verification pipeline. The paper details the CHC-to-CFA transformation, CEGAR-based abstraction with two abstract domains, and a suite of bounded and diagram-based techniques that are integrated via a sequential portfolio. It also discusses model generation, software architecture, and a corrected re-evaluation on CHC-COMP benchmarks, highlighting improvements after fixing a misconfiguration. The findings demonstrate Theta’s competitive performance on linear CHCs and emphasize the value of modular design for scalable CHC solving in practice.

Abstract

Theta is a verification framework that has participated in the CHC-COMP competition since 2023. While its core approach -- based on transforming constrained Horn clauses (CHCs) into control-flow automata (CFAs) for analysis -- has remained mostly unchanged, Theta's verification techniques, design trade-offs, and limitations have remained mostly unexplored in the context of CHCs. This paper fills that gap: we provide a detailed description of the algorithms employed by Theta, highlighting the unique features that distinguish it from other CHC solvers. We also analyze the strengths and weaknesses of the tool in the context of CHC-COMP benchmarks. Notably, in the 2025 edition of the competition, Theta's performance was impacted by a configuration issue, leading to suboptimal results. To provide a clearer picture of Theta's actual capabilities, we re-execute the tool on the competition benchmarks under corrected settings and report on the resulting performance.

Paper Structure

This paper contains 26 sections, 1 equation, 5 figures, 2 tables.

Table of Contents

  1. Funding.
  2. Introduction
  3. Verification Approach
  4. CHC-to-CFA Transformation
  5. CEGAR-based Verification
  6. Abstract Domain
  7. Explicit Domain.
  8. Predicate Domain.
  9. Refinement Algorithm
  10. Bounded, Property-Directed and Decision-Diagram-Based Techniques
  11. Bounded Techniques
  12. Property-Directed Reachability
  13. Decision-Diagram-Based Techniques
  14. CHC-Solvers as Backend
  15. Portfolio Strategy
  16. ...and 11 more sections

Figures (5)

  • Figure 1: The CEGAR loop
  • Figure 2: An ARG
  • Figure 3: Substitution diagram characterizing the initial states $I: x = 0 \land y = x$ (left) and 2k-level substitution diagram characterizing the transition relation $T: x' = x + 1 \land y' = x$ (right). Each level has an associated variable, nodes correspond to SMT formulas, while the edges represent substituting the variable of the current level with a literal value in the SMT formula of the source node. We omit edges leading to the terminal $\bot$ node. The diagram on the right has infinitely many edges leaving the top node, we only display $0$ and $5$ for readability.
  • Figure 4: Quantile plots of configurations in the linear categories
  • Figure : The CEGAR loop