Ultimate TreeAutomizer (CHC-COMP Tool Description)

TL;DR

Ultimate TreeAutomizer is a solver for satisfiability of constrained Horn clauses, utilizing trace abstraction, tree automata, and interpolation, presented as a tool for CHC-COMP 2019.

Contribution

It introduces Ultimate TreeAutomizer, a novel solver combining trace abstraction, tree automata, and interpolation for CHC satisfiability.

Findings

Successfully participated in CHC-COMP 2019.

Demonstrates effectiveness of combined techniques.

Provides a detailed tool description for the community.

Abstract

We present Ultimate TreeAutomizer, a solver for satisfiability of sets of constrained Horn clauses. Constrained Horn clauses (CHC) are a fragment of first order logic with attractive properties in terms of expressiveness and accessibility to algorithmic solving. Ultimate TreeAutomizer is based on the techniques of trace abstraction, tree automata and tree interpolation. This paper serves as a tool description for TreeAutomizer in CHC-COMP 2019.

Equations

$$\forall \vec{x}.C(\vec{x})\to$$

$$\forall \vec{x}.P_{\_}1(\vec{x})\wedge \dots \wedge P_{\_}n(\vec{x})\wedge C(\vec{x})\to$$

$$\forall \vec{x}.C_{\_}1(\vec{x})\wedge \dots \wedge C_{\_}n(\vec{x})\to \mathsf{false}$$

Full text

1 Introduction

We present \ultimate\treeautomizer, a solver for satisfiability of sets of constrained Horn clauses. The logical fragment of constrained Horn clauses (CHC) has received increasing attention in the last years. One reason for its attractiveness in program verification is that it naturally allows for expressing proof queries for many kinds of correctness proofs, e.g., classic Floyd-Hoare proofs for while-programs, but also assume-guarantee reasoning, compositional verification, and many more [12, 16].

The CHC fragment is equivalent in expressive power to the verification of safety properties of procedural (possibly recursive) programs, i.e., there is a translation of a CHC-formula to a procedural program such that the CHC-formula is satisfiable if and only if the procedural program is correct, and vice versa. Therefore, it is not surprising that solvers for CHC-formulas often adapt algorithms known in program verification. For example, HSF [11, 4] uses predicate abstraction, Spacer111https://spacer.bitbucket.io uses PDR [10, 15], and Rahft [18] uses trace abstraction [13], to name just a few tools. \ultimate\treeautomizeris part of this tradition and is an adaptation of the trace abstraction verification algorithm for procedural programs [14].

This paper is a tool description for the \treeautomizertool as it participated in \chccompin 2018 and 2019. We give a brief overview of how trace abstraction is used to solve CHC-formulas. Afterwards, we describe some aspects of the implementation of \treeautomizerand some crucial optimizations. Last, we discuss expected strengths and weaknesses of the approach.

2 Approach

In this section, we describe the approach for solving formulas in the CHC-fragment used in \treeautomizer. The approach is based on trace abstraction [13]; its adaptation to solving CHC-formulas has been described by Kafle and Gallagher [17] and by Wang and Jiao [20], we refer to these papers for a more in-depth description and only give an overview here.

In the following, we assume that a constraint theory $T$ is given, and that we have an SMT-solver for $T$. Furthermore, we refer to constraints over theory $T$ with free variables $\vec{x}$ as $C(\vec{x})$ and we assume that a set $\{P_{\_}1,P_{\_}2,\ldots\}$ of predicate symbols is given that are not used by the constraint theory $T$.

A formula in the CHC-fragment is given as a set of clauses where each clause is of one of the below forms. According to general convention, Horn clauses subdivided the categories of facts, definite clauses, and queries (also: goal clauses), depending on which of the below patterns they match.

[TABLE]

In the remainder, we assume that a set $S$ of constrained Horn clauses is given.

Now, let us consider the resolution trees over the clauses in set $S$ with root $\mathsf{false}$. We call such a tree a derivation of $\mathsf{false}$. Since no constraints ever occur in a clause head, the resolvent at the root of a derivation of $\mathsf{false}$ is a query with one large conjunctive constraint in the antecedent, i.e., it is of the following form.

[TABLE]

We call a derivation of $\mathsf{false}$ feasible if the formula $\exists\vec{x}\ldotp C_{\_}1(\vec{x})\land\ldots\land C_{\_}n(\vec{x})$ is satisfiable, and infeasible otherwise. The existence of a feasible derivation of $\mathsf{false}$ means that the conjunction of the clauses in $S$ is contradictory. Completeness of first-order resolution implies that the converse also holds, i.e., that the absence of a feasible derivation of $\mathsf{false}$ implies satisfiability of the formula. Thus, we can formulate the following proof rule.

A set of constraint Horn clauses $S$ is satisfiable if and only if there is no feasible derivation of $\mathsf{false}$ over $S$.

\ultimate\treeautomizer

’s approach to prove satisfiability of the set of Horn clauses $S$ is to show infeasibility of all derivations of $\mathsf{false}$ over $S$. The refinement algorithm used for this purpose is shown in Figure 1. The proving process starts by sampling a derivation from the set of all derivations of $\mathsf{false}$ over $S$. The sample derivation is then checked for feasibility using an SMT solver. If the sample derivation is feasible, the clause set $S$ is unsatisfiable (since it implies $\mathsf{false}$). If the sample derivation is infeasible, the sample is generalized to a set of derivations which are all infeasible. This set is subtracted from the set of derivations of $\mathsf{false}$. This process is repeated until either all derivations of $\mathsf{false}$ have been proven infeasible or a feasible derivation has been found.

3 Implementation

\treeautomizer

is implemented in the \ultimateframework. It is written in Java, open source, and can be downloaded and contributed to on \ultimate’s Github page222https://github.com/ultimate-pa/.

\ultimate

provides for \treeautomizerthe SMTLIB parser, utilities for handling formulas (e.g., simplifications), and the \ultimateAutomata Library. SMT solvers for which by \ultimateprovides an interface include SMTInterpol [5], Z3 [19], CVC4 [3], and MathSat [6]. In cases when a solver does not support interpolation in the given constraint theory, but can produce unsatisfiable cores, Newton-style interpolation [9] can be used to obtain interpolants.

\treeautomizer

takes as input Horn clause sets in the format used in \chccomp333https://chc-comp.github.io/2018/format.html. During parsing, the input formulas are converted into the normal form given above.

In order to represent (possibly infinite) sets of derivations of $\mathsf{false}$, \treeautomizeruses tree automata (see [8] for more details on tree automata). The alphabet that the tree automata operate on is the set of input Horn clauses $S$. The states of the tree automata have one of two different semantics. The states of the automata A, and $A_{S}$ represent the uninterpreted predicates in the set $\{P_{\_}1,P_{\_}2\ldots\}$. The states of the interpolant automaton G represent the interpolants from the interpolation query that is generated from the sample derivation of $\mathsf{false}$ d. From this sample query, a generalization procedure computes the canonical interpolant automaton. The canonical interpolant automaton is given by the set of all rules that correspond to a valid implication between the formulas in the source of the automaton rules, the constraint in the alphabet symbol, and the formula at target of the rule (see [20]) for a thorough description).

4 Optimizations

In each iteration of the main refinement loop of trace abstraction, an interpolant automaton (G) is created and subtracted from the automaton representing the derivations of $\mathsf{false}$ (A). Two major bottlenecks in terms of space and time consumption may arise from this. First, the generalization that is done during creation of the interpolant automaton can produce a large number of candidate transition rules each one requiring an SMT solver call. Second, the difference operation requires construction of a product automaton and thus can lead to growth of the automaton representing the derivations of $\mathsf{false}$ that is exponential in the number of loop iterations. Both problems are amplified by an increasing nonlinearity of the involved Horn clauses.

Minimization

The explosion through the repeated product construction can often be contained through an additional minimization step on the result of the difference operation. Standard minimization algorithms for tree automata can be used here; the \ultimateautomata library currently supports two minimization variants, one based on the naive algorithm [8] the other on bisimulation [2].

On-Demand Construction of Interpolant Automaton

The explosion of the number of rules in the interpolant automaton can be countered by integrating the difference (i.e., complementation and intersection) operation with the creation of the interpolant automaton.

The idea behind the integration is that a large number of candidate rules in the interpolant automaton is irrelevant to the result of the difference operation. The basic intuition here is that for computing the difference $S\setminus T$ of two sets $S$ and $T$, only the part of $T$ that lies in the intersection of $S$ and $T$ is relevant – elements of $T$ that don’t lie in $S$ need not be considered by a subtraction algorithm. For the subtraction of tree automata, this means the following: A rule is irrelevant to the result of the difference operation, $\texttt{A}-\texttt{G}$, if it never contributes to the construction of a tree in G that lies in the language of A. Such candidate rules can be filtered out during the product construction by only querying the interpolant automaton for rules whose source tuple is reachable in according to the minuend automaton (A).

5 Discussion

\treeautomizer

’s approach inherits its basic properties from the trace abstraction approach. Thus, \treeautomizeris conceptually sound and relatively complete. As is common for such refinement schemes, the actual detection of a proof of satisfiability (and thus actual completeness) depends on guessing the right formulas during the generalization step (we only mentioned interpolation here, but several other methods are available).

We believe that one strength of the trace abstraction approach lies in a semantic independence of refinement steps. For example in predicate abstraction with CEGAR [7] (which several program verification schemes can be seen as a variant of), formulas that stem from many different refinement steps are conjoined. This means that SMT-solver queries get bigger and bigger over a growing number of iterations, which can swamp the SMT solver. In trace abstraction on the other hand, the formulas used in the generalize procedure can be forgotten, after the difference A - G has been computed, i.e. formulas from different refinement steps are never conjoined. However, among other things, this property relies on a rich-enough structure of the initial automaton. In particular, this means that CHC-formulas that stem from proof queries for programs where large block encoding has been performed or where the program counter is not made explicit by using different uninterpreted predicates for each location, this compositionality may not come into full effect.