Source-linked AI summary
Symbolic Execution of Constrained Horn Clauses
Johannes Weiser, Zafer Esen, Philipp Rümmer
TL;DR
CHC verification uses model-checking algorithms, and constrained resolution offers a simpler alternative for reasoning about CHC satisfiability. The paper formalizes its correspondence to forward and backward symbolic execution; experiments find the two directions complementary and show the approach is viable despite minimal subsumption and no search heuristics.
Problem
CHC solvers use varied model-checking algorithms, motivating a simpler alternative for analyzing CHC satisfiability.
Source: §1 · p. 2Method
The paper formalizes forward and backward constrained-resolution strategies as symbolic execution over CHCs and develops subsumption criteria for pruning derivations.
Source: §1 · p. 2, §7 · p. 20Results
Forward and backward symbolic execution are often complementary across benchmark categories, and symbolic execution remains viable without subsumption beyond syntactic identity checks or search heuristics.
Source: §9.2 · pp. 25–27Takeaways & Limitations
Constrained resolution avoids relatively expensive steps such as Craig interpolation and can be implemented for complex theories such as arrays or bit-vectors.
Source: §1 · p. 2Expressing the determinism condition in formula (25) generally requires existentially quantified Horn clauses, beyond CHCs and unsupported by existing CHC solvers.
Source: §8 · p. 23
Abstract
from arXiv · showhide
Constrained Horn clauses (CHCs) are a fragment of first-order logic widely used as an intermediate language for verification. We study constrained resolution as a calculus for reasoning about the satisfiability of sets of CHCs. Constrained resolution forms a simple alternative to model checking algorithms such as CEGAR and IC3 and is here shown to exhibit complementary features. We show that, when CHCs encode programs, forward symbolic execution corresponds to positive unit hyper-resolution, and backward symbolic execution to SLD resolution, which are special cases of constrained resolution. We formalize forward and backward reasoning for linear and non-linear CHCs and transition systems, prove refutational completeness under fair strategies, and develop subsumption criteria for pruning redundant derivations. We moreover show that backward resolution with subsumption generalizes $k$-induction to non-linear CHCs, and that forward constrained resolution is related to the problem of constructing proofs in incorrectness logic. Lastly, we provide an experimental evaluation in the Eldarica CHC solver on benchmarks from CHC-COMP.
1 Introduction
The paper presents constrained resolution as a simple alternative for analyzing CHCs and makes explicit how its forward and backward strategies correspond to symbolic execution. A motivating loop shows forward reasoning finding an assertion violation, while backward reasoning with subsumption proves safety when forward expansion does not terminate.
1 Introduction
- Constrained resolution is a simpler alternative to model-checking algorithms such as CEGAR and IC3, with symbolic execution effective at finding bugs and proving correctness.It avoids relatively expensive steps such as Craig interpolation and can be implemented for theories including arrays or bit-vectors.Source: §1 · p. 2
- Forward symbolic execution corresponds to constrained positive unit hyper-resolution, while backward symbolic execution corresponds to SLD resolution.The paper formalizes both strategies for linear and non-linear CHCs and studies subsumption for pruning redundant derivations.Source: §1 · p. 2
- Backward resolution with subsumption generalizes k-induction and applies to non-linear clauses.Backward reasoning implicitly constructs the conditions checked by k-induction.Source: §1 · p. 2
- Forward resolution proofs for program-encoding CHCs translate into incorrectness-logic proofs, including non-ground proofs.The connection also permits translating bespoke incorrectness rules, such as loop acceleration, into the CHC setting.Source: §1 · p. 3
1.1 Motivating Example
- The motivating program encodes its loop-head states with q(x, b, x0), and its assertion as a goal clause.The variable b records the loop branch, while x0 tracks the initial value of x.Source: §1.1 · p. 3
- With P(x, x0) = (x = x0), forward resolution derives an unsatisfiable clause after one iteration, exposing an assertion violation.The derived state has x = x0 + 2, which cannot satisfy the assertion x = x0.Source: §1.1 · p. 4
- With P(x, x0) = (x ≥ x0), forward resolution's chain grows indefinitely, but backward resolution with subsumption terminates and proves safety.Subsumed predecessor clauses add no information, and the remaining checks are discharged against the initial state.Source: §1.1 · pp. 5–6
2 Preliminaries
The preliminaries establish the first-order logic and CHC vocabulary, then introduce resolution and its constrained variant for deriving consequences and proving unsatisfiability.
2.1 First-Order Logic
- First-order logic represents formulas with sorted terms, atoms, connectives, and quantifiers, interpreted over structures and a fixed background theory.A theory entailment must hold across its structures and extensions; the article uses ⊨ for entailment in its fixed theory.Source: §2.1 · p. 6
2.2 Constrained Horn Clauses (CHCs)
- A CHC has at most one positive literal and a background-theory constraint; facts, rules, and goals are distinguished by their heads and bodies.CHCs are linear when their bodies contain at most one uninterpreted atom, and non-linear otherwise.Source: §2.2 · p. 7
2.3 Calculi and Resolution
- Resolution derives a resolvent from clauses with complementary literals, and deriving the empty clause establishes unsatisfiability.A calculus is refutation-complete when every unsatisfiable clause set admits a finite derivation of the empty clause.Source: §2.3 · p. 7
First-Order Resolution
- First-order resolution makes the resolved atoms identical through unification, using a most general unifier to form the resolvent.The example substitutes x with a and y with b, yielding r(a) ∨ s(b).Source: First-Order Resolution · p. 8
Constrained Resolution
- Constrained resolution replaces syntactic unification with an equality constraint checked in the background theory, accommodating theory-interpreted terms.In the example, simplifying the added equalities yields q(x0+2, 1, x0) ← ⊤.Source: Constrained Resolution · p. 8
3 Symbolic Execution as Resolution
Symbolic execution explores program paths using symbolic states and path conditions; constrained unit resolution represents those states as CHCs. Forward and backward search correspond to different resolution strategies, with fairness and clause shape affecting completeness.
Symbolic Execution
- Symbolic execution branches over control flow while accumulating path conditions, and checks at assertions whether a feasible symbolic state can violate the property.Unsatisfiable path conditions identify infeasible paths; the tree can contain infinite paths for non-terminating executions.Source: §3 · pp. 9–10
Symbolic Execution as Resolution
- Symbolic states correspond to derivable CHCs under constrained unit resolution, while assertion failure corresponds to deriving an unsatisfiable clause.Derived clauses omit the relation between initial and intermediate states unless ghost variables record the initial state.Source: §3 · p. 10
Search Strategies
- Fair strategies such as breadth-first search are refutationally complete, whereas depth-first search is incomplete for non-linear clauses.Fair saturation with subsumption can also construct the least model and prove satisfiability, including for programs with unbounded loops.Source: §3 · p. 10
Backward Resolution
- Backward resolution starts from goals and derives obligations at earlier locations; SLD resolution is the appropriate form for non-linear clauses.Backward unit resolution is incomplete for non-linear clauses even with fair application strategies; backward reasoning can show satisfiability where forward strategies diverge.Source: §3 · pp. 10–11
4 Forward Execution by Unit Hyper-Resolution
Forward Execution (FE) uses unit hyper-resolution to explore CHCs from initial facts. Under fair strategies it is refutationally complete, and termination with SAT supports model construction.
4 Forward Execution by Unit Hyper-Resolution
- FE is bottom-up evaluation corresponding to symbolic execution from the initial state, using unit hyper-resolution to derive facts.The calculus combines constrained resolution with hyper-resolution, so its consequences are facts.Source: §4 · p. 11, §4.1 · p. 11
4.1 The Algorithm of FE
- FE avoids deriving facts deemed redundant by a subsumption procedure that soundly and decidably approximates semantic entailment.The procedure must terminate and recognize clause membership; the algorithm checks for contradictions and for remaining nonredundant derivations.Source: §4.1 · pp. 11–12
4.2 Refutational Completeness of FE
- With a fair strategy, FE is refutationally complete: it terminates with UNSAT if and only if the CHC set is unsatisfiable.Fairness ensures that eligible nonredundant facts are eventually covered by a subsuming state.Source: §4.2 · p. 13
4.3 Constructing Models from FE
- When FE terminates with SAT, interpreting each predicate with the facts in its final state gives the least model of the CHC set.FE is sound for both UNSAT and SAT outcomes, and its final pre-SAT state supports model extraction.Source: §4.3 · pp. 13–14
5 Backward Execution by Hyper-SLD-Resolution
Backward execution (BE) starts from goals and resolves them against rules, extending SLD resolution with hyper-SLD-resolution and redundancy pruning. Under fair strategies BE is refutationally complete, while its stated model-construction result is restricted to linear goals.
5.1 The Algorithm of BE
- Hyper-SLD-resolution generalizes SLD-resolution so BE can add redundancy pruning while retaining a basis for refutational completeness.Ordinary SLD-resolution is the special case that resolves one atom; hyper-SLD-resolution permits several controlled resolutions at once.Source: §5.1 · p. 14
- BE unfolds goals by adding hyper-SLD resolvents not subsumed by existing goals, and returns UNSAT or SAT according to conflict and subsumption checks.The abstract transition system leaves the choice of which goals to add to the strategy.Source: §5.1 · p. 15, §5.2 · p. 15
- In Example 3, resolving the nonlinear even-number goal produces a linear odd-number goal, and continued resolution derives a contradiction.The other branch is explored but not shown.Source: §5.1 · p. 15
5.2 Refutational Completeness of BE
- Unlike ordinary SLD-resolution, hyper-SLD-resolution is monotone with respect to logical entailment, a property used in the completeness argument.The paper gives an example where logically equivalent goals yield non-equivalent sets of ordinary SLD resolvents.Source: §5.2 · pp. 16–17
- Under a fair strategy, BE terminates with UNSAT exactly when its input CHC set is unsatisfiable.The proof relies on hyper-SLD-resolution being monotone with respect to logical entailment.Source: §5.2 · p. 17
5.3 Constructing Models from BE
- When BE terminates with SAT and all saturated goals are linear, interpreting each predicate from those goals gives the greatest model.The paper leaves model construction for the general case open; nonlinear goals create dependencies between predicate interpretations, and a greatest fixed point need not exist.Source: §5.3 · p. 18
6 Backward Execution vs. k-Induction
The paper compares BE with k-induction, which is formulated for a restricted form of CHC sets. Under a completeness condition on subsumption, BE matches the k-induction checks there and extends the approach to arbitrary CHC sets.
6 Backward Execution vs. k-Induction
- For the restricted CHC form, k-induction checks a safe base case of paths up to length k and a consecution step for paths of length k+1.The paper notes that transition systems can be translated into this form.Source: §6 · p. 19
- The paper reports no known formulation of k-induction for nonlinear goals in the more general setting.Its straightforward formulation applies to the specified restricted clause form.Source: §6 · p. 19
- For this fragment, BE's checks match k-induction precisely when subsumption is complete for the relevant goal clauses.BE's conflict check corresponds to the base case, and absence of further non-subsumed goals corresponds to the induction step.Source: §6 · p. 19
- Unlike classical k-induction's linear-clause restriction, BE applies to arbitrary CHC sets, including nonlinear ones.The paper presents BE as a natural extension of k-induction in that general setting.Source: §6 · pp. 19–20
7 Subsumption
The paper develops decidable subsumption criteria as practical approximations to logical entailment, which is undecidable in general. It shows that disjunctive subsumption is complete for facts and goals, but not for arbitrary clause sets.
7 Subsumption
- Subsumption approximates entailment because direct first-order entailment checks are undecidable, and the paper presents decidable criteria of varying strength.These criteria serve as redundancy checks in the forward and backward algorithms.Source: §7 · p. 20
- θ-subsumption requires one variable substitution to witness entailment, so it can miss cases where different instances establish the entailment.For example, an odd sum entails that one summand is odd, but no fixed substitution identifies which one.Source: §7 · p. 20
- Disjunctive subsumption is sound and stronger than plain subsumption, yet some clause sets entail a clause without disjunctively subsuming it.Combining information across clauses can capture cases missed by single-clause subsumption, but the method still does not capture all entailments.Source: §7 · pp. 21–22
- For finite sets of facts and for sets of goals, disjunctive subsumption holds exactly when the set entails the target clause.These completeness results do not extend to general clause sets.Source: §7 · p. 22
8 Symbolic Execution and Incorrectness Logic
The section connects constrained-resolution proofs of program behavior to incorrectness logic, including symbolic proofs and a loop-variant rule. It also identifies where CHC encodings of incorrectness reasoning are limited.
Incorrectness logic
- Incorrectness logic reasons about failing executions, but its existential condition makes encoding general incorrectness triples as CHCs nontrivial.For injective statements, the formula can be expressed as a CHC; the general case requires existentially quantified Horn clauses outside standard CHCs.Source: §8 · pp. 22–23
Constrained proof rules
- The forward rule is sound exactly when ψ[¯x′] implies that some ¯x satisfies φ[¯x] and TS(¯x, ¯x′).This condition ties the proposed postcondition to a predecessor state and the statement transition.Source: §8 · pp. 23–24
Proof translation
- Forward symbolic-execution proofs translate into incorrectness-logic proofs using derived constrained facts, and backward proofs can be translated through forward proofs.The result clauses of incorrectness triples are the derived constrained positive unit clauses.Source: §8 · p. 24
- Symbolic execution can yield non-ground incorrectness proofs because its proofs need not refer to concrete values.The paper also notes that specialized incorrectness proof rules can be extended to CHC proofs.Source: §8 · p. 24
Proof rules for loops
- A backward-variant rule generalizes a fact from n = 0 to n ≥ 0 when the constraint is a variant that decreases through the loop body backwards.A refined calculus that generalizes such derivations is left for future work.Source: §8 · p. 24
9 Experiments
The Eldarica experiments compare forward and backward symbolic execution with CEGAR across CHC-COMP categories. Symbolic execution is viable and often complementary across directions, although the search strategy affects which instances are solved.
9.1 Setup
- The evaluation implemented forward and backward execution in Eldarica and tested five configurations on nine CHC-COMP 2026 categories.The configurations included CEGAR, CEGAR without interpolation abstraction, forward BFS and DFS, and backward BFS; DFS supported only linear CHCs.Source: §9 · p. 24, §9.1 · p. 25
9.2 Results and Discussion
- Table 1 summarizes satisfiable and unsatisfiable instances solved per category, while Tables 2 and 3 provide pairwise comparisons.Table 1 marks the best values for each category; Tables 2 and 3 cover non-linear and linear categories, respectively.Source: §9.2 · p. 25, Table 1 · p. 25, Table 2 · p. 26
- Forward and backward symbolic execution often solve different instances across categories, and BEBFS is often more effective than FEBFS on satisfiable instances.The comparison tables report pairwise counts of instances solved by a row configuration but not a column configuration.Source: §9.2 · p. 25, Table 2 · p. 26, Table 3 · p. 26
- 11 satisfiable instances in ADT-LIA-Arrays and 20 in LIA-Lin were solved only by FEBFS.These are examples of instances solved only by symbolic execution configurations.Source: §9.2 · p. 26
- DFS solves fewer instances overall but sometimes finds unsatisfiable instances that other strategies miss.It can find deep refutations, but can also remain on an infinitely deep branch that yields no refutation.Source: §9.2 · p. 26
- Symbolic execution is a viable CHC-solving approach, substantially simpler to implement than CEGAR or IC3, even without broader subsumption or search heuristics.The implemented configurations only checked for identical resolvents; the evaluation compared them with Eldarica’s CEGAR engine.Source: §9.1 · p. 25, §9.2 · pp. 26–27
10 Related Work
The related work contrasts invariant-synthesis and resolution-based CHC solvers, then situates constrained resolution among symbolic execution, k-induction, acceleration, and logic-programming resolution.
10.1 CHC Solving and Software Model Checking
- Many CHC solvers synthesize invariants: Spacer uses IC3 with interpolation and model-based projection, Eldarica uses CEGAR with predicate abstraction, and Golem includes transition power abstraction.Transition power abstraction builds increasingly deep over-approximations using interpolation.Source: §10.1 · p. 27
- Constrained resolution avoids invariant synthesis: its forward clauses encode reachable states, while backward clauses encode proof obligations.Eldarica implements both directions; Golem implements forward symbolic execution for linear CHCs.Source: §10.1 · p. 27
- Backward resolution with subsumption generalizes k-induction to non-linear clauses without a separate fold/unfold transformation.Bjørner et al. recast k-induction as such a transformation for linear CHCs.Source: §10.1 · p. 27
- Like acceleration-driven clause learning, constrained resolution is refutationally complete and can prove satisfiability, but it does not necessarily terminate.Acceleration-driven clause learning adds clauses that simulate arbitrarily many applications of a recursive clause in one step.Source: §10.1 · p. 27
10.2 Resolution and Logic Programming
- Constrained resolution replaces syntactic unification with background-theory equality constraints, while SLD resolution restricts backward resolution to definite clauses with a selection rule.Forward execution corresponds to bottom-up logic-program evaluation and backward execution to top-down evaluation; CHC models and refutations represent correctness proofs and failing executions, respectively.Source: §10.2 · p. 28
11 Conclusion
The conclusion frames constrained resolution as a foundation for further symbolic-execution strategies, while noting challenges in adapting concolic execution and the practical cost of subsumption.
Future work
- Adapting concolic execution to CHCs is not straightforward because CHCs lack a fixed notion of input variables to concretize.One proposed option is to strengthen constraints when the SMT solver cannot decide satisfiability within a time limit.Source: §11 · p. 28
- Iterative deepening, generational search, and bidirectional strategies remain possible directions for exploration.The paper notes that forward and backward execution are complementary in practice.Source: §11 · p. 28
- Subsumption checks may be useful, but their cost depends on the background theory and can be expensive in practice.The conclusion identifies subsumption as a potential aid rather than an implemented general solution.Source: §11 · p. 28