Horn Clause Solvers for Program Verification

Abstract

Automatic program verification and symbolic model checking tools interface with theorem proving technologies that check satisfiability of formulas. A theme pursued in the past years by the authors of this paper has been to encode symbolic model problems directly as Horn clauses and develop dedicated solvers for Horn clauses. Our solvers are called Duality, HSF, SeaHorn, and $\mu {Z}$ and we have devoted considerable attention in recent papers to algorithms for solving Horn clauses. This paper complements these strides as we summarize main useful properties of Horn clauses, illustrate encodings of procedural program verification into Horn clauses and then highlight a number of useful simplification strategies at the level of Horn clauses. Solving Horn clauses amounts to establishing Existential positive Fixed-point Logic formulas, a perspective that was promoted by Blass and Gurevich.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

We make the overall claim that Constrained Horn Clauses provide a suitable basis for automatic program verification, that is, symbolic model checking. To substantiate this claim, this paper provides a self-contained, but narrowly selected, account for the use of Horn clauses in symbolic model checking. It is based on experiences the authors had while building tools for solving Horn clauses. At the practical level, we have been advocating the use of uniform formats, such as the SMT-LIB [6] standard as a format for representing and exchanging symbolic model checking problems as Horn clauses. The authors and many of our colleagues have developed several tools over the past years that solve Horn clauses in this format. We illustrate three approaches, taken from Duality, SeaHorn and HSF, for translating procedural programs into Horn clauses. At the conceptual level, Horn clause solving provides a uniform setting where we can discuss algorithms for symbolic model checking. This uniform setting allows us to consider integration of separate algorithms that operate as transformations of Horn clauses. We illustrate three transformations based on recent symbolic model checking literature and analyze them with respect to how they simplify the task of fully solving clauses. As a common feature, we show how solutions to the simplified clauses can be translated back to original clauses by means of Craig interpolation [22].

1.1 Program Logics and Horn Clauses

Blass and Gurevich [15] made the case that Existential positive Least Fixed-point Logic (E+LFP) provides a logical match for Hoare logic: Partial correctness of simple procedural imperative programs correspond to satisfiability in E+LFP. We can take this result as a starting point for our focus on Horn clauses. As we show in Sect. 2.1, the negation of an E+LFP formula can be written as set of Horn clauses, such that the negation of an E+LFP formula is false if and only if the corresponding Horn clauses are satisfiable.

The connections between Constrained Horn Clauses and program logics originates with Floyd-Hoare logic [29, 37, 53]. Cook’s [21] result on relative completeness with respect to Peano arithmetic established that Hoare’s axioms were complete for safety properties relative to arithmetic. Clarke [20] established boundaries for relative completeness. Cook’s result was refined by Blass and Gurevich.

In the world of constraint logic programming, CLP, expressing programs as Horn clauses and reasoning about Horn clauses has been pursued for several years, spearheaded by Joxan Jaffar and collaborators [41]. The uses of CLP for program analysis is extensive and we can only mention a few other uses of CLP for program analysis throughout the paper. Note that the more typical objective in constraint logic programming [2, 42] is to use logic as a declarative programming language. It relies on an execution engine that finds a set of answers, that is a set of substitutions that are solutions to a query. In an top-down evaluation engine, each such substitution is extracted from a refutation proof.

In the world of deductive databases [19], bottom-up evaluation of Datalog programs has, in addition to top-down, been explored extensively. Bottom-up evaluation infers consequences from facts and project the consequences that intersect with a query. Each such intersection corresponds to a refutation proof of a statement of the form “query is unreachable”. Note that if the intersection is empty, then the smallest set of consequences closed under a Datalog program is a least model of the program and negated query.

Rybalchenko demonstrated how standard proof rules from program verification readily correspond to Horn clauses [32], and we have since been promoting constrained Horn clauses as a basis for program analysis [12].

1.2 Paper Outline

Figure 1 summarizes a use of Horn clauses in a verification workflow. Sections 3 and 4 detail translation of programs into clauses and simplifying transformations on clauses, respectively. Section 2 treat Horn clause basics. It is beyond the scope of this paper to go into depth of any of the contemporary methods for solving clauses, although this is central to the overall picture.

Fig. 1.

Horn clause verification flow

In more detail, in Sect. 2, we recall the main styles of Horn clauses used in recent literature and tools. We also outline contemporary methods for solving clauses that use strategies based on combinations of top-down and bottom-up search. As the main objective of solving Horn clauses is to show satisfiability, in contrast to showing that there is a derivation of the empty clause, we introduce a notion of models definable modulo an assertion language. We call these symbolic models. Many (but not all) tools for Horn clauses search for symbolic models that can be represented in a decidable assertion language. Note that symbolic models are simply synonymous to loop invariants, and [16] demonstrated that decidable assertion languages are insufficient for even a class of very simple programs. Section 3 compares some of the main approaches use for converting procedural programs into clauses. The approaches take different starting points on how they encode procedure calls and program assertions and we discuss how the resulting Horn clauses can be related. Section 4 summarizes three selected approaches for transforming Horn clauses. Section 4.1 recounts a query-answer transformation used by Gallagher and Kafle in recent work [30, 46]. In Sect. 4.2 we recall the well-known fold-unfold transformation and use this setting to recast K-induction [64] in the form of a Horn clause transformation. Section 4.3 discusses a recently proposed optimization for simplifying symbolic model checking problems [49]. We show how the simplification amounts to a rewriting strategy of Horn clauses. We examine each of the above transformation techniques under the lens of symbolic models, and address how they influence the existence and complexity of such models. The treatment reveals a common trait: the transformations we examine preserve symbolic models if the assertion language admits interpolation.

2 Horn Clause Basics

Let us first describe constrained Horn clauses and their variants. We take the overall perspective that constrained Horn clauses correspond to a fragment of first-order formulas modulo background theories.

We will assume that the constraints in constrained Horn Clauses are formulated in an assertion language that we refer to as $\mathcal {A}$. In the terminology of CLP, an assertion language is a constraint theory. In the terminology of SMT, an assertion language is a logic [6]. The terminology assertion language is borrowed from [52]. Typically, we let $\mathcal {A}$ be quantifier-free (integer) linear arithmetic. Other examples of $\mathcal {A}$ include quantifier-free bit-vector formulas and quantifier-free formulas over a combination of arrays, bit-vectors and linear arithmetic. Interpretations of formulas over $\mathcal {A}$ are defined by theories. For example, integer linear arithmetic can be defined by the signature $\langle Z, +, \le \rangle$, where Z is an enumerable set of constants interpreted as the integers, $+$ is a binary function and $\le$ is a binary predicate over integers interpreted as addition and the linear ordering on integers.

Schematic examples of constrained Horn clauses are

$$\begin{aligned} \forall x, y, z\ .\ q(y) \wedge r(z) \wedge \varphi (x,y,z) \rightarrow p(x,y) \end{aligned}$$

and

$$\begin{aligned} \forall x, y, z\ .\ q(y) \wedge r(z) \wedge \varphi (x,y,z) \rightarrow \psi (z,x) \end{aligned}$$

where p, q, r are predicate symbols of various arities applied to variables x, y, z and $\varphi , \psi$ are formulas over an assertion language $\mathcal {A}$. More formally,

Definition 1

(CHC: Constrained Horn Clauses). Constrained Horn clauses are constructed as follows:

$$\begin{aligned} \varPi&{:}{:}{=} \, chc \wedge \varPi \mid \top \\ chc&{:}{:}{=}\, \forall var \ . \ chc \mid body \rightarrow head \\ pred&{:}{:}{=}\, upred \mid \varphi \\ head&{:}{:}{=}\, pred \\ body&{:}{:}{=}\, \top \mid pred \mid body \wedge body \mid \exists var \ . \ body \\ upred&{:}{:}{=}\, \text{ an } \text{ uninterpreted } \text{ predicate } \text{ applied } \text{ to } \text{ terms } \\ \varphi&{:}{:}{=}\, \text{ a } \text{ formula } \text{ whose } \text{ terms } \text{ and } \text{ predicates } \text{ are } \text{ interpreted } \text{ over } \mathcal {A} \\ var&{:}{:}{=}\, \text{ a } \text{ variable } \end{aligned}$$

We use P, Q, R as uninterpreted atomic predicates and B, C as bodies. A clause where the head is a formula $\varphi$ is called a query or a goal clause. Conversely we use the terminology fact clause for a clause whose head is an uninterpreted predicate and body is a formula $\varphi$.

Note that constrained Horn clauses correspond to clauses that have at most one positive occurrence of an uninterpreted predicate. We use $\varPi$ for a conjunction of constrained Horn clauses and chc to refer to a single constrained Horn clause.

Convention 1

In the spirit of logic programming, we write Horn clauses as rules and keep quantification over variables implicit. Thus, we use the two representations interchangeably:

$$\begin{aligned} \begin{array}{llll} \forall x, y, z\ .\ q(y) \wedge r(z) \wedge \varphi (x, y,z) \rightarrow p(x)&\quad \quad \text{ as } \quad \quad&\,&p(x) \leftarrow q(y), r(z), \varphi (x, y,z) \end{array} \end{aligned}$$

Example 1

Partial correctness for a property of the McCarthy 91 function can be encoded using the clauses

$$\begin{aligned} mc(x,r)\leftarrow & {} x > 100, r = x - 10 \\ mc(x,r)\leftarrow & {} x \le 100, y = x + 11, mc(y,z), mc(z,r) \\ r = 91\leftarrow & {} mc(x,r), x \le 101 \end{aligned}$$

The first two clauses encode McCarthy 91 as a constraint logic program. The last clause encodes the integrity constraint stipulating that whenever the McCarthy 91 function is passed an argument no greater than 101, then the result is 91.

Some formulas that are not directly Horn can be transformed into Horn clauses using a satisfiability preserving Tseitin transformation. For example, we can convert¹

$$\begin{aligned} p(x)\leftarrow & {} (q(y) \vee r(z)), \varphi (x,y,z) \end{aligned}$$

(1)

into

$$\begin{aligned} s(y,z) \leftarrow q(y) \quad \quad&s(y,z) \leftarrow r(z) \quad \quad&p(x) \leftarrow s(y,z), \varphi (x,y,z) \end{aligned}$$

(2)

by introducing an auxiliary predicate s(y, z).

A wider set of formulas that admit an equi-satisfiable transformation to constrained Horn clauses is given where the body can be brought into negation normal form, NNF, and the head is a predicate or, recursively, a conjunction of clauses. When we later in Sect. 3 translate programs into clauses, we will see that NNF Horn clauses fit as a direct target language. So let us define the class of NNF Horn clauses as follows:

Definition 2

(NNF Horn)

$$\begin{aligned} \varPi&{:}{:}{=}\, chc \wedge \varPi \mid \top \\ chc&{:}{:}{=} \, \forall var \ . \ chc \mid body \rightarrow \varPi \mid head \\ head&{:}{:}{=} \, pred \\ body&{:}{:}{=} \, body \vee body \mid body \wedge body \mid pred \mid \exists var \ . \ body \\ \end{aligned}$$

The previous example suggests there is an overhead associated with converting into constrained Horn clauses.

Proposition 1

NNF Horn clauses with n sub-formulas and m variables can be converted into O(n) new Horn clauses each using O(m) variables.

Thus, the size of the new formulas is $O(n\cdot m)$ when converting NNF Horn clauses into Horn clauses. The asymptotic overhead can be avoided by introducing a theory of tupling with projection and instead pass a single variable to intermediary formulas. For the formula (1), we would create the clauses:

$$\begin{aligned} s(u) \leftarrow q(\pi _1(u)) \quad \quad&s(u) \leftarrow r(\pi _2(u)) \quad \quad&p(x) \leftarrow s(\langle y,z\rangle ), \varphi (x,y,z) \end{aligned}$$

(3)

where $\pi _1, \pi _2$ take the first and second projection from a tuple variable u, and the notation $\langle x, y\rangle$ is used to create a tuple out of x and y.

Several assertion languages used in practice have canonical models. For example, arithmetic without division has a unique standard model. On the other hand, if we include division, then division by 0 is typically left under-specified and there is not a unique model, but many models, for formulas such as $x/0 > 0$.

Recall the notion of convexity [55], here adapted to Horn clauses. We will establish that Horn clauses and an extension called universal Horn clauses are convex. We show that a further extension, called existential Horn clauses, is not convex as an indication of the additional power offered by existential Horn clauses. Let $\varPi$ be a set of Horn clauses, then $\varPi$ is convex if for every pair of uninterpreted atomic predicates P, Q:

$$\begin{aligned} \varPi ~\models ~ P \vee Q \ \ \ \text{ iff } \ \ \ \varPi ~\models ~P \ \text{ or } \ \varPi ~\models ~Q \end{aligned}$$

Proposition 2

Suppose $\mathcal {A}$ has a canonical model $\mathcal {I}(\mathcal {A})$, then Horn clauses over $\mathcal {A}$, where each head is an uninterpreted predicate, are convex.

The proposition is an easy consequence of

Proposition 3

Constrained Horn clauses over assertion languages $\mathcal {A}$ that have canonical models have unique least models.

This fact is a well known basis of Horn clauses  [25, 40, 67]. It can be established by closure of models under intersection, or as we do here, by induction on derivations:

Proof

Let $\mathcal {I}(\mathcal {A})$ be the canonical model of $\mathcal {A}$. The initial model $\mathcal {I}$ of $\varPi$ is defined inductively by taking $\mathcal {I}_0$ as $\emptyset$ and $\mathcal {I}_{i+1} := \{ r(c) \mid (r(x) \leftarrow body (x)) \in \varPi , \mathcal {I}_i ~\models ~ body (c), \ c { is} { a} { constant} { in} \mathcal {I}(\mathcal {A}) \}$. The initial model construction stabilizes at the first limit ordinal $\omega$ with an interpretation $\mathcal {I}_{\omega }$. This interpretation satisfies each clause in $\varPi$ because suppose $(r(x) \leftarrow body (x)) \in \varPi$ and $\mathcal {I}_{\omega } ~\models ~ body (c)$ for $c \in \mathcal {I}(\mathcal {A})$. Then, since the body has a finite set of predicates, for some ordinal $\alpha < \omega$ it is the case that $\mathcal {I}_{\alpha } ~\models ~ body (c)$ as well, therefore r(c) is added to $\mathcal {I}_{\alpha +1}$.

To see that Proposition 2 is a consequence of least unique models, consider a least unique model $\mathcal {I}$ of Horn clauses $\varPi$, then $\mathcal {I}$ implies either P or Q or both, so every extension of $\mathcal {I}$ implies the same atomic predicate.

While constrained Horn clauses suffice directly for Hoare logic, we applied two kinds of extensions for parametric program analysis and termination. We used universal Horn clauses to encode templates for verifying properties of array-based systems [14].

Definition 3

(UHC). Universal Horn clauses extend Horn clauses by admitting universally quantifiers in bodies. Thus, the body of a universal Horn clause is given by:

$$\begin{aligned} body&{:}{:}{=}\, \top \mid body \wedge body \mid pred \mid \forall var \ . \ body \mid \exists var \ . \ body \end{aligned}$$

Proposition 4

Universal Horn clauses are convex.

Proof

The proof is similar as constrained Horn clauses, but the construction of the initial model does not finish at $\omega$, see for instance [14, 15]. Instead, we treat universal quantifiers in bodies as infinitary conjunctions over elements in the domain of $\mathcal {I}(\mathcal {A})$ and as we follow the argument from Proposition 3, we add r(c) to the least ordinal greater than the ordinals used to establish the predicates in the bodies.

Existential Horn clauses can be used for encoding reachability games [9].

Definition 4

(EHC). Existential Horn clauses extend Horn clauses by admitting existential quantifications in the head:

$$\begin{aligned} head&{:}{:}{=} \, \exists var \ . \ head \mid pred \end{aligned}$$

Game formalizations involve handling fixed-point formulas that alternate least and greatest fixed-points. This makes it quite difficult to express using formalisms, such as UHC, that are geared towards solving only least fixed-points. So, as we can expect, the class of EHC formulas is rather general:

Proposition 5

EHC is expressively equivalent to general universally quantified formulas over $\mathcal {A}$.

Proof

We provide a proof by example. The clause $\forall x, y \ . \ p(x,y) \vee q(x) \vee \lnot r(y)$, can be encoded as three EHC clauses

$$\begin{aligned} \begin{array}{lll} (\exists z \in \{ 0, 1 \}\ . \ s(x,y,z)) \leftarrow r(y) \quad \quad&p(x,y) \leftarrow s(x,y,0)\quad \quad&q(x) \leftarrow s(x,y,1) \end{array} \end{aligned}$$

We can also directly encode satisfiability of UHC using EHC by Skolemizing universal quantifiers in the body. The resulting Skolem functions can be converted into Skolem relations by creating relations with one additional argument for the return value of the function, and adding clauses that enforce that the relations encode total functions. For example, $p(x) \leftarrow \forall y \ . \ q(x,y)$ becomes $p(x) \leftarrow sk(x,y), q(x,y)$, and $(\exists y \ . \ sk(x,y)) \leftarrow q(x,y)$. Note that (by using standard polarity reasoning, similar to our Tseitin transformation of NNF clauses) clauses that enforce sk to be functional, e.g., $y = y' \leftarrow sk(x,y), sk(x,y')$ are redundant because sk is introduced for a negative sub-formula.

As an easy corollary of Proposition 5 we get

Corollary 1

Existential Horn clauses are not convex.

2.1 Existential Fixed-Point Logic and Horn Clauses

Blass and Gurevich [15] identified Existential Positive Fixed-point Logic (E+LFP) as a match for Hoare Logic. They established a set of fundamental model theoretic and complexity theoretic results for E+LFP. Let us here briefly recall E+LFP and the main connection to Horn clauses. For our purposes we will assume that least fixed-point formulas are flat, that is, they use the fixed-point operator at the top-level without any nesting. It is not difficult to convert formulas with arbitrary nestings into flat formulas, or even convert formulas with multiple simultaneous definitions into a single recursive definition for that matter. Thus, using the notation from [15], a flat E+LFP formula $\varTheta$ is of the form:

$$\begin{aligned} \varTheta: & {} \mathbf{LET}\ \bigwedge _i p_i(x) \leftarrow \delta _i(x)\ \mathbf{THEN}\ \varphi \end{aligned}$$

where $p_i,\delta _i$ range over mutually defined predicates and neither $\delta _i$ nor $\varphi$ contain any LET constructs. Furthermore, each occurrence of $p_i$ in $\delta _j$, respectively $\varphi$ is positive, and $\delta _j$ and $\varphi$ only contain existential quantifiers under an even number of negations. Since every occurrence of the uninterpreted predicate symbols is positive we can convert the negation of a flat E+LFP formula to NNF-Horn clauses as follows:

$$\begin{aligned} \varTheta ': & {} \bigwedge _i \forall x (\delta _i(x) \rightarrow p_i(x)) \wedge (\varphi \rightarrow \bot ) \end{aligned}$$

Theorem 1

Let $\varTheta$ be a flat closed E+LFP formula. Then $\varTheta$ is equivalent to false if and only if the associated Horn clauses $\varTheta '$ are satisfiable.

Proof

We rely on the equivalence:

$$\begin{aligned} \lnot (\mathbf{LET}\ \bigwedge _i p_i(x) \leftarrow \delta _i(x)\ \mathbf{THEN}\ \varphi )\equiv & {} \exists \mathbf {p} \ . \ (\bigwedge _i \forall x \ . \ \delta _i(x) \rightarrow p_i(x)) \wedge \lnot \varphi [\mathbf {p}] \end{aligned}$$

where $\mathbf {p}$ is a vector of the predicate symbols $p_i$. Since all occurrences of $p_i$ are negative, when some solution for $\mathbf {p}$ satisfies the fixed-point equations, and also satisfies $\lnot \varphi [\mathbf {p}]$, then the least solution to the fixed-point equations also satisfies $\lnot \varphi [\mathbf {p}]$.

Another way of establishing the correspondence is to invoke Theorem 5 from [15], which translates E+LFP formulas into $\forall _1^1$ formulas. The negation is an $\exists ^1_1$ Horn formula.

Remark 1

The logic U+LFP, defined in [15], is similar to our UHC. The differences are mainly syntactic in that UHC allows alternating universal and existential quantifiers, but U+LFP does not.

2.2 Derivations and Interpretations

Horn clauses naturally encode the set of reachable states of sequential programs, so satisfiable Horn clauses are program properties that hold. In contrast, unsatisfiable Horn clauses correspond to violated program properties. As one would expect, it only requires a finite trace to show that a program property does not hold. The finite trace is justified by a sequence of resolution steps, and in particular for Horn clauses, it is sufficient to search for SLD [2] style proofs. We call these top-down derivations.

Definition 5

(Top-down Derivations). A top-down derivation starts with a goal clause of the form $\varphi \leftarrow B$. It selects a predicate $p(x)\in B$ and resolves it with a clause $p(x) \leftarrow B' \in \varPi$, producing the clause $\varphi \leftarrow B\setminus p(x), B'$, modulo renaming of variables in B and $B'$. The derivation concludes when there are no predicates in the goal, and the clause is false modulo $\mathcal {A}$.

That is, top-down inferences maintain a goal clause with only negative predicates and resolve a negative predicate in the goal with a clause in $\varPi$. Top-down methods based on infinite descent or cyclic induction close sub-goals when they are implied by parent sub-goals. Top-down methods can also use interpolants or inductive generalization, in the style of the IC3 algorithm [17], to close sub-goals. In contrast to top-down derivations, bottom-up derivations start with clauses that have no predicates in the bodies:

Definition 6

(Bottom-up Derivations). A bottom-up derivation maintains a set of fact clauses of the form $p(x) \leftarrow \varphi$. It then applies hyper-resolution on clauses ($head \leftarrow B) \in \varPi$, resolving away all predicates in B using fact clauses. The clauses are inconsistent if it derives a contradictory fact clause (which has a formula from $\mathcal {A}$ in the head).

Bottom-up derivations are useful when working with abstract domains that have join and widening operations. Join and widening are operations over an abstract domain (encoded as an assertion language $\mathcal {A}$) that take two formulas $\varphi$ and $\varphi '$ and create a consequence that is entailed by both.

For constrained Horn clauses we have

Proposition 6

(unsat is r.e.). Let $\mathcal {A}$ be an assertion language where satisfiability is recursively enumerable. Then unsatisfiability for constrained Horn clauses over $\mathcal {A}$ is r.e.

Proof

Recall the model construction from Proposition 3. Take the initial model of the subset of clauses that have uninterpreted predicates in the head. Checking membership in the initial model is r.e., because each member is justified at level $\mathcal {I}_i$ for some $i < \omega$. If the initial model also separates from $\bot$, then the clauses are satisfiable. So assuming the clauses are unsatisfiable there is a finite justification (corresponding to an SLD resolution derivation [2]), of $\bot$. The constraints from $\mathcal {A}$ along the SLD chain are satisfiable.

From the point of view of program analysis, refutation proof corresponds to a sequence of steps leading to a bad state, a bug. Program proving is much harder that finding bugs: satisfiability for Horn clauses is generally not r.e.

Definition 7

( $\mathcal {A}$ -Definable Models). Let $\mathcal {A}$ be an assertion language, an $\mathcal {A}$-definable model assigns to each predicate p(x) a formula $\varphi (x)$ over the language of $\mathcal {A}$.

Example 2

A linear arithmetic-definable model for the mc predicate in Example 1 is as follows:

$$\begin{aligned} mc(x,y):= & {} y \ge 91 \wedge (y \le 91 \vee y \le x - 10) \end{aligned}$$

We can verify that the symbolic model for mc satisfies the original three Horn clauses. For example, $x > 100 \wedge y = x - 10$ implies that $y > 100 - 10$, so $y \ge 91$ and $y \le x - 10$. Thus, $mc(x,r)\leftarrow x > 10, r = x - 10$ is true.

Presburger arithmetic and additive real arithmetic are not expressive enough to define all models of recursive Horn clauses, for example one can define multiplication using Horn clauses and use this to define properties not expressible with addition alone [16, 63]. When working with assertion languages, such as Presburger arithmetic we are interested in more refined notions of completeness:

Definition 8

( $\mathcal {A}$ -Preservation). A satisfiability preserving transformation of Horn clauses from $\varPi$ to $\varPi '$ is $\mathcal {A}$-preserving if $\varPi$ has an $\mathcal {A}$-definable model if and only if $\varPi '$ has an $\mathcal {A}$-definable model.

We are also interested in algorithms that are complete relative to $\mathcal {A}$. That is, if there is an $\mathcal {A}$-definable model, they will find one. In [47] we identify a class of universal sentences in the Bernays Schoenfinkel class and an associated algorithm that is relatively complete for the fragment. In a different context Revesz identifies classes of vector addition systems that can be captured in Datalog [61]. In [11] we investigate completeness as a relative notion between search methods based on abstract interpretation and property directed reachability.

2.3 Loose Semantics and Horn Clauses

A formula $\varphi$ is satisfiable modulo a background theory $\mathcal {T}$ means that there is an interpretation that satisfies the axioms of $\mathcal {T}$ and the formula $\varphi$ (with free variables x). Thus, in Satisfiability Modulo Theories jargon, the queries are of the form

$$\begin{aligned} \exists f \ . \ \mathcal {A}x(f)\ \wedge \ \exists x \ . \ \varphi \end{aligned}$$

(4)

where f are the functions defined for the theory $\mathcal {T}$ whose axioms are $\mathcal {A}x$. The second-order existential quantification over f is of course benign because the formula inside the quantifier is equi-satisfiable.

When the axioms have a canonical model, this condition is equivalent to

$$\begin{aligned} \forall f \ . \ \mathcal {A}x(f)\ \rightarrow \ \exists x \ . \ \varphi \end{aligned}$$

(5)

In the context of Horn clause satisfiability, the format (5) captures the proper semantics. To see why, suppose $unk$ is a global unknown array that is initialized by some procedure we can’t model, and consider the following code snippet and let us determine whether it is safe.

$$\begin{aligned} \ell _0: \mathbf{if}\ ( unk [x] > 0)\ \mathbf{goto}\ :error \end{aligned}$$

In this example, the interpretation of the array unknown is not fully specified. So there could be an interpretation of unknown where the error path is not taken. For example, if $\ell _0$ is reached under a context where $unk [x]$ is known to always be non-positive, the program is safe. Consider one possible way to translate this snippet into Horn clauses that we denote by $Safe (\ell _0, unk )$:

$$\begin{aligned} \forall x \ . \ (\top \rightarrow \ell _0(x))&\wedge&(\ell _0(x) \wedge unk [x] > 0 \rightarrow \bot ). \end{aligned}$$

These clauses are satisfiable. For example, we can interpret the uninterpreted predicates and functions as follows: $unk := const (0)$, $\ell _0(x) := \top$, where we use $const (0)$ for the array that constantly returns 0. This is probably not what we want. For all that we know, the program is not safe. Proper semantics is obtained by quantifying over all loose models. This amounts to checking satisfiability of:

$$\begin{aligned} \forall unk \exists \ell _0\ .\ Safe (\ell _0, unk ) \end{aligned}$$

which is equi-satisfiable to:

$$\begin{aligned} \forall unk , x \ . \ ((\top \rightarrow \ell _0( unk ,x)) \quad \wedge \quad (\ell _0( unk ,x) \wedge unk [x] > 0 \rightarrow \bot )). \end{aligned}$$

which is easily seen to be false by instantiating with $unk := const (1)$.

3 From Programs to Clauses

The are many different ways to transition from programs to clauses. This section surveys a few of approaches used in the literature and in tools. The conceptually simplest way to establish a link between checking a partial correctness property in a programming language and a formulation as Horn clauses is to formulate an operational semantics as an interpreter in a constraint logic program and then specialize the interpreter when given a program. This approach is used in the VeriMAP [24] tool an by [30]. The methods surveyed here bypass the interpreter and produce Horn clauses directly. Note that it is not just sequential programs that are amenable to an embedding into Horn clauses. One can for instance model a network of routers as Horn clauses [51].

3.1 State Machines

A state machine starts with an initial configuration of state variables $\mathbf {v}$ and transform these by a sequence of steps. When the initial states and steps are expressed as formulas $init (\mathbf {v})$ and $step (\mathbf {v},\mathbf {v}')$, respectively, then we can check safety of a state machine relatively to a formula $safe (\mathbf {v})$ by finding an inductive invariant $inv (\mathbf {v})$ such that [52]:

$$\begin{aligned} inv (\mathbf {v}) \leftarrow init (\mathbf {v}) \quad&inv (\mathbf {v}') \leftarrow inv (\mathbf {v}) \wedge step (\mathbf {v},\mathbf {v}') \quad&safe (\mathbf {v}) \leftarrow inv (\mathbf {v}) \end{aligned}$$

(6)

3.2 Procedural Languages

Safety of programs with procedure calls can also be translated to Horn clauses. Let us here use a programming language substrate in the style of the Boogie [4] system:

$$\begin{aligned} program&{:}{:}{=} \, decl ^* \\ decl&{:}{:}{=} \, \mathbf {def}\ p(x)\ \{\ \mathbf{local}\ \mathbf {v}; S\ \} \\ S&{:}{:}{=} \, x := E\;\mid \; S_1; S_2\; \mid \; \mathbf{if}\ E \ \mathbf{then}\ S_1\ \mathbf{else}\ S_2 \mid \; S_1 \Box S_2 \\&\; \mid \,\,\,\; \mathbf{havoc}\ x\; \mid \; \mathbf{assert}\ E\; \mid \; \mathbf{assume}\ E\; \\&\; \mid \,\,\,\; \mathbf{while} \ E \ \mathbf{do}\ S \; \mid \; y := p(E) \; \mid \; \mathbf{goto}\ \ell \; \mid \; \ell : S\\ E&{:}{:}{=} \, \text{ arithmetic } \text{ logical } \text{ expression } \end{aligned}$$

In other words, a program is a set of procedure declarations. For simplicity of presentation, we restrict each procedure to a single argument x, local variables $\mathbf {v}$ and a single return variable $ret$. Most constructs are naturally found in standard procedural languages. The non-conventional havoc(x) command changes x to an arbitrary value, and the statement $S_1 \Box S_2$ non-deterministically chooses run either $S_1$ or $S_2$. We use $\mathbf {w}$ for the set of all variables in the scope of a procedure. For brevity, we write procedure declarations as $\mathbf {def}\ p(x)\ \{ S \}$ and leave the return and local variable declarations implicit. All methods generalize to procedures that modify global state and take and return multiple values, but we suppress handling this here. We assume there is a special procedure called $main$, for the main entry point of the program. Notice that assertions are included in the programming language.

Consider the program schema in Fig. 2. The behavior of procedure q is defined by the formula $\psi$, and other formulas $init , \varphi _1, \varphi _2$ are used for pre- and post-conditions.

Fig. 2.

Sample program with procedure calls

Weakest Preconditions. If we apply Boogie directly we obtain a translation from programs to Horn logic using a weakest liberal pre-condition calculus [26]:

$$\begin{aligned} {\mathsf {ToHorn}}( program ):= & {} wlp ( Main (), \top ) \wedge \bigwedge _{ decl \in program } {\mathsf {ToHorn}}( decl ) \\ {\mathsf {ToHorn}}(\mathbf {def}\ p(x)\ \{ S \}):= & {} wlp \left( \begin{array}{ll} \mathbf{havoc}\ x_0; \mathbf{assume}\ x_0 = x; \\ \mathbf{assume}\ p_{pre}(x); S, \ &{} p(x_0, ret ) \end{array}\right) \\ wlp (x := E, Q):= & {} \mathbf{let}\ x = E\ \mathbf{in}\ Q \\ wlp ((\mathbf{if}\ E\ \mathbf{then}\ S_1\ \mathbf{else}\ S_2), Q):= & {} wlp (((\mathbf{assume}\ E; S_1) \Box (\mathbf{assume}\ \lnot E; S_2)), Q) \\ wlp ((S_1 \Box S_2), Q):= & {} wlp (S_1, Q) \wedge wlp (S_2, Q) \\ wlp (S_1;S_2, Q):= & {} wlp (S_1, wlp (S_2, Q)) \\ wlp (\mathbf{havoc}\ x, Q):= & {} \forall x \ . \ Q \\ wlp (\mathbf{assert}\ \varphi , Q):= & {} \varphi \wedge Q \\ wlp (\mathbf{assume}\ \varphi , Q):= & {} \varphi \rightarrow Q \\ wlp ((\mathbf{while}\ E\ \mathbf{do}\ S), Q):= & {} inv (\mathbf {w}) \wedge \\&\forall \mathbf {w} \ . \ \left( \begin{array}{ll} &{} (( inv (\mathbf {w}) \wedge E)\ \rightarrow \ wlp (S, inv (\mathbf {w}))) \\ \wedge &{} (( inv (\mathbf {w}) \wedge \lnot E)\ \rightarrow \ Q) \end{array} \right) \\ wlp (y := p(E), Q):= & {} p_{pre}(E) \wedge (\forall r \ . \ p(E,r) \ \rightarrow \ Q[r/y])\\ wlp (\mathbf{goto}\ \ell , Q):= & {} \ell (\mathbf {w}) \wedge Q \\ wlp (\ell : S, Q):= & {} wlp(S,Q) \wedge (\forall \mathbf {w} \ . \ \ell (\mathbf {w}) \rightarrow wlp(S,Q)) \end{aligned}$$

The rule for $\Box$ duplicates the formula Q, and when applied directly can cause the resulting formula to be exponentially larger than the original program. Efficient handling of join-points has been the attention of a substantial amount of research around large block encodings [10] and optimized verification condition generation [5, 28, 33, 50]. The gist is to determine when to introduce auxiliary predicates for join-points to find a sweet spot between formula size and ease of solvability. Auxiliary predicates can be introduced as follows:

$$\begin{aligned} wlp ((S_1 \Box S_2), Q):= & {} wlp (S_1, p(\mathbf {w})) \wedge wlp (S_2, p(\mathbf {w})) \wedge \forall \mathbf {w} \ . \ (p(\mathbf {w}) \rightarrow Q) \end{aligned}$$

Procedures can be encoded as clauses in the following way: A procedure p(x) is summarized as a relation $p(x, ret )$, where x is the value passed into the procedure and the return value is $ret$.

Proposition 7

Let $prog$ be a program. The formula ${\mathsf {ToHorn}}( prog )$ is NNF Horn.

Proof

By induction on the definition of $wlp$.

Example 3

When we apply ${\mathsf {ToHorn}}$ to the program in Fig. 2 we obtain a set of Horn clauses:

$$\begin{aligned} main (x)\leftarrow & {} \top \\ \varphi _1(y)\leftarrow & {} main (x), init (x), p(x,z), p(z, y) \\ p_{pre}(x)\leftarrow & {} main (x), init (x) \\ p_{pre}(z)\leftarrow & {} main (x), init (x), p(x,z) \\ p(x,y) \wedge \varphi _2(y)\leftarrow & {} p_{pre}(x), q(x,z), q(z,y) \\ q_{pre}(x)\leftarrow & {} p_{pre}(x) \\ q_{pre}(z)\leftarrow & {} p_{pre}(x), q(x,z) \\ q(x,y)\leftarrow & {} q_{pre}(x), \psi (x,y) \end{aligned}$$

Error Flag Propagation. The SeaHorn verification system [34] uses a special parameter to track errors. It takes as starting point programs where asserts have been replaced by procedure calls to a designated error handler $error$. That is, assert $\varphi$ statements are replaced by if $\lnot \varphi$ then $error ()$. Furthermore, it assumes that each procedure is described by a set of control-flow edges, i.e., statements of the form $\ell _{in}: S; \mathbf{goto }\, \ell _{out}$, where S is restricted to a sequential composition of assignments, assumptions, and function calls.

To translate procedure declarations of the form $\mathbf {def}\ p(x)\ \{\ S\ \}$, SeaHorn uses procedure summaries of the form

$$\begin{aligned} p(x, ret , e_{i}, e_{o}), \end{aligned}$$

where $ret$ is the return value, and the flags $e_{i}, e_{o}$ track the error status at entry and the error status at exit. If $e_{i}$ is true, then the error status is transferred. Thus, for every procedure, we have the fact:

$$\begin{aligned} p(x, ret, \top , \top )\leftarrow & {} \top . \end{aligned}$$

In addition, for the error procedure, we have:

$$\begin{aligned} error (e_{i}, e_{o})\leftarrow & {} e_{o}. \end{aligned}$$

We will use $wlp$ to give meaning to basic statements here as well, using the duality of $wlp$ and pre-image. To translate procedure calls that now take additional arguments we require to change the definition of $wlp$ as follows:

$$\begin{aligned} wlp (y := p(E), Q):= & {} \forall r, err \ . \ p(E, r, e_{i}, err ) \rightarrow Q[r/y, err /e_{i}]. \end{aligned}$$

where $err$ is a new global variable that tracks the value of the error flag.

Procedures are translated one control flow edge at a time. Each label $\ell$ is associated with a predicate $\ell (x_0, \mathbf {w}, e_{o})$. Additionally, the entry of a procedure p is labeled by the predicate $p_{init}(x_0, \mathbf {w}, e_{o})$ and the exit of a procedure is labeled by a predicate $p_{exit}(x_0, ret , e_{o})$. An edge links its entry $\ell _{in}(x_0, \mathbf {w}, e_{o})$ with its exit $\ell _{out}(x_0,\mathbf {w}',e_{o}')$, which is an entry point into successor edges. The rules associated with the edges are formulated as follows:

$$\begin{aligned} p_{init}(x_0, \mathbf {w}, \bot )\leftarrow & {} x = x_0 \quad \quad \quad \text{ where } \text{ x } \text{ occurs } \text{ in } \mathbf {w}\\ p_{exit}(x_0, ret , \top )\leftarrow & {} \ell (x_0, \mathbf {w}, \top ) \quad \text{ for } \text{ each } \text{ label } \ell \text{, } \text{ and } ret \text{ occurs } \text{ in } \mathbf {w}\\ p(x, ret , \bot , \bot )\leftarrow & {} p_{exit}(x, ret , \bot ) \\ p(x, ret , \bot , \top )\leftarrow & {} p_{exit}(x, ret , \top ) \\ \ell _{out}(x_0, \mathbf {w}', e_{o})\leftarrow & {} \ell _{in}(x_0, \mathbf {w}, e_{i}) \wedge \lnot e_{i}\wedge \lnot wlp (S, \lnot (e_{i}= e_{o}\wedge \mathbf {w} = \mathbf {w}')) \end{aligned}$$

A program is safe if the clauses compiled from the program together with:

$$\begin{aligned} \bot\leftarrow & {} Main _{exit}(x, ret , \top ) \end{aligned}$$

are satisfiable.

Example 4

When we create clauses directly from program in Fig. 2 we get the following set of clauses:

$$\begin{aligned} \bot\leftarrow & {} main (\bot , \top ) \\ main (e_{i}, e_{o})\leftarrow & {} init (x), p(x,z,e_{i}, e_{o}'), p(y, z, e_{o}', e_{o}''), \lnot \varphi _1(y), error (e_{o}'', e_{o}) \\ main (e_{i}, e_{o})\leftarrow & {} init (x), p(x,y,e_{i}, e_{o}'), p(y, z, e_{o}', e_{o}), \varphi _1(y) \\ p(x,ret, e_{i}, e_{o})\leftarrow & {} q(x,z,e_{i}, e_{o}'), q(z,ret, e_{o}', e_{o}''), \lnot \varphi _2(ret), error (e_{o}'',e_{o})\\ p(x,ret, e_{i}, e_{o})\leftarrow & {} q(x,z,e_{i}, e_{o}'), q(z,ret, e_{o}', e_{o}), \varphi _2(ret) \\ q(x,ret, e_{i}, e_{o})\leftarrow & {} \psi (x, ret), e_{i}= e_{o}\\ p(x,ret, \top , \top )\leftarrow & {} \top \\ q(x,ret, \top , \top )\leftarrow & {} \top \\ main (\top , \top )\leftarrow & {} \top \\ error (e_{i}, e_{o})\leftarrow & {} e_{o}\end{aligned}$$

Transition Summaries. The HSF tool [32] uses summary predicates that capture relations between the program variables at initial locations of procedures and their values at a program locations within the same calling context. Transition summaries are useful for establishing termination properties. Their encoding captures the well-known RHS (Reps-Horwitz-Sagiv) algorithm [3, 60] that relies on top-down propagation with tabling (for use of tabling in logic programming, see for instance [68]). Thus, let $\mathbf {w}$ be the variables x, $ret$, local variables $\mathbf {v}$ and program location $\pi$ for a procedure p. Then the translation into Horn clauses uses predicates of the form:

$$\begin{aligned} p(\mathbf {w}, \mathbf {w}'). \end{aligned}$$

To translate a procedure call $\ell : y := q(E); \ell '$ within a procedure p, create the clauses:

$$\begin{aligned} p(\mathbf {w}_0, \mathbf {w}_4)\leftarrow & {} p(\mathbf {w}_0, \mathbf {w}_1), call (\mathbf {w}_1,\mathbf {w}_2), q(\mathbf {w}_2, \mathbf {w}_3), return (\mathbf {w}_1,\mathbf {w}_3,\mathbf {w}_4) \\ q(\mathbf {w}_2, \mathbf {w}_2)\leftarrow & {} p(\mathbf {w}_0, \mathbf {w}_1), call (\mathbf {w}_1,\mathbf {w}_2)\\ call (\mathbf {w},\mathbf {w}')\leftarrow & {} \pi = \ell , x' = E, \pi ' = \ell _{q_{init}}\\ return (\mathbf {w}, \mathbf {w}',\mathbf {w}'')\leftarrow & {} \pi ' = \ell _{q_{exit}}, \mathbf {w}'' = \mathbf {w}[ret'/y, \ell '/\pi ] \end{aligned}$$

The first clause establishes that a state $\mathbf {w}_4$ is reachable from initial state $\mathbf {w}_0$ if there is a state $\mathbf {w}_1$ that reaches a procedure call to q and following the return of q the state variables have been updated to $\mathbf {w}_4$. The second clause summarizes the starting points of procedure q. So, if p can start at state $\mathbf {w}_0$ For assertion statements $\ell : \mathbf{assert}\ \varphi ; \ell '$, produce the clauses:

$$\begin{aligned} \varphi (\mathbf {w})\leftarrow & {} p(\mathbf {w}_0, \mathbf {w}), \pi = \ell \\ p(\mathbf {w}_0, \mathbf {w}[\ell '/\pi ])\leftarrow & {} p(\mathbf {w}_0, \mathbf {w}), \pi = \ell , \varphi (\mathbf {w}) \end{aligned}$$

Other statements are broken into basic blocks similar to the error flag encoding. For each basic block $\ell : S; \ell '$ in procedure p create the clause:

$$\begin{aligned} p(\mathbf {w}_0,\mathbf {w}'')\leftarrow & {} p(\mathbf {w}_0,\mathbf {w}), \pi _0 = \ell , \pi '' = \ell ', \lnot wlp (S, (\mathbf {w} \ne \mathbf {w}'')) \end{aligned}$$

Finally, add the following clause for the initial states:

$$\begin{aligned} main (\mathbf {w},\mathbf {w})\leftarrow & {} \pi = \ell _{ main _{init}} . \end{aligned}$$

Note that transition summaries are essentially the same as what we get from ${\mathsf {ToHorn}}$. The main difference is that one encoding uses program labels as state variables, the other uses predicates. Otherwise, one can extract the pre-condition for a procedure from the states that satisfy $p(\mathbf {w},\mathbf {w})$, and similarly the post-condition as the states that satisfy $p(\mathbf {w},\mathbf {w}') \wedge \pi ' = \ell _{exit}$. Conversely, given solutions to $p_{pre}$ and p, and the predicates summarizing intermediary locations within p one can define a summary predicate for p by introducing program locations.

3.3 Proof Rules

The translations from programs to Horn clauses can be used when the purpose is to to check assertions of sequential programs. This methodology, however is insufficient for dealing with concurrent programs with recursive procedures, and there are other scenarios where Horn clauses are a by-product of establishing program properties. The perspective laid out in [32] is that Horn clauses are really a way to write down search for intermediary assertions in proof rules as constraint satisfaction problems. For example, many proof rules for establishing termination, temporal properties, for refinement type checking, or for rely-guarantee reasoning can be encoded also as Horn clauses.

As an example, consider the rules (6) for establishing invariants of state machines. If we can establish that each reachable step is well-founded, we can also establish termination of the state machine. That is, we may ask to solve for the additional constraints:

$$\begin{aligned} round(v, v') \leftarrow inv (v) \wedge step (v,v').&\quad&wellFounded (round). \end{aligned}$$

(7)

The well-foundedness constraint on $round$ can be enforced by restricting the search space of solutions for the predicate to only well-founded relations.

Note that in general a proof rule may not necessarily be complete for establishing a class of properties. This means that the Horn clauses that are created as a side-effect of translating proof rules to clauses may be unsatisfiable while the original property still holds.

4 Solving Horn Clauses

A number of sophisticated methods have recently been developed for solving Horn clauses. These are described in depth in several papers, including [11, 23, 24, 27, 32, 38, 43, 48, 54, 63]. We will not attempt any detailed survey of these methods here, but just mention that most methods can be classified according to some main criteria first mentioned in Sect. 2.2:

• 1. Top-down derivations. In the spirit of SLD resolution, start with a goal and resolve the goals with clauses. Derivations are cut off by using cyclic induction or interpolants. If the methods for cutting off all derivation attempts, one can extract models from the failed derivation attempts. Examples of tools based on top-down derivation are [38, 48, 54].

• 2. Bottom-up derivations start with clauses that don’t have uninterpreted predicates in the bodies. They then derive consequences until sufficiently strong consequences have been established to satisfy the clauses. Examples of tools based on bottom-up derivation are [32].

• 3. Transformations change the set of clauses in various ways that are neither top-down nor bottom-up directed.

We devote our attention in this section to treat a few clausal transformation techniques. Transformation techniques are often sufficiently strong to solve clauses directly, but they can also be used as pre-processing or in-processing techniques in other methods. As pre-processing techniques, they can significantly simplify Horn clauses generated from tools [8] and they can be used to bring clauses into a useful form that enables inferring useful consequences [46].

4.1 Magic Sets

The query-answer transformation [30, 46], a variant of the Magic-set transformation [68], takes a set of horn clauses $\varPi$ and converts it into another set $\varPi ^{qa}$ such that bottom-up evaluation in $\varPi ^{qa}$ simulates top down evaluation of of $\varPi$. This can be an advantage in declarative data-bases as the bottom-up evaluation of the transformed program avoids filling intermediary tables with elements that are irrelevant to a given query. In the context of solving Horn clauses, the advantage of the transformation is that the transformation captures some of the calling context dependencies making bottom-up analysis more precise.

The transformation first replaces each clause of the form $\varphi \leftarrow B$ in $\varPi$ by a clause $g \leftarrow B, \lnot \varphi$, where g is a fresh uninterpreted goal predicate. It then adds the goal clauses $g^q \leftarrow \top$, $\bot \leftarrow g^a$ for each goal predicate g. We use the super-scripts a and q in order to create two fresh symbols for each symbol. Finally, for $p(x) \leftarrow P_1, \ldots , P_n, \varphi$ in $\varPi$ the transformation adds the following clauses in $\varPi ^{qa}$:

• Answer clause: $p^a(x) \leftarrow p^q(x), P_1^a, \ldots , P_n^a, \varphi$

• Query clauses: $P^q_{j} \leftarrow p^q(x), P_1^a, \ldots , P_{j-1}^a, \varphi$ for $j = 1, \ldots , n$.

Where, by $P_1, \ldots , P_n$ are predicates $p_1, \ldots , p_n$ applied to their arguments. Given a set of clauses $\varPi$, we call the clauses that result from the transformation just described $\varPi ^{qa}$.

A symbolic solution to the resulting set of clauses $\varPi ^{qa}$ can be converted into a symbolic solution for the original clause $\varPi$ and conversely.

Proposition 8

Given a symbolic solution $\varphi ^q,$ $\varphi ^a,$ $\psi _1^q,$ $\psi _1^a, \ldots ,$ $\psi _n^q,$ $\psi _n^a$, to the predicates $p, p_1, \ldots , p_n$, then $p(x) := \varphi ^q \rightarrow \varphi ^a,$ $P_1 := \psi _1^q \rightarrow \psi _1^a,$ $\ldots ,$ $P_n := \psi _n^q \rightarrow \psi _n^a$ solves $p(x) \leftarrow P_1, \ldots , P_n, \varphi$. Conversely, any solution to the original clauses can be converted into a solution of the Magic clauses by setting the query predicates to $\top$ and using the solution for the answer predicates.

Note how the Magic set transformation essentially inserts pre-conditions into procedure calls very much in the same fashion that the ${\mathsf {ToHorn}}$ and the transition invariant translation incorporates pre-conditions to procedure calls.

Remark 2

Sect. 4.3 describes transformations that eliminate pre-conditions from procedure calls. In some way, the Magic set transformation acts inversely to eliminating pre-conditions.

4.2 Fold/Unfold

The fold/unfold transformation [18, 65, 66] is also actively used in systems that check satisfiability of Horn clauses [36, 57] as well as in the partial evaluation literature [45].

The unfold transformation resolves each positive occurrence of a predicate with all negative occurrences. For example, it takes a system of the form

$$\begin{aligned} \begin{array}{l} q(y) \leftarrow B_1 \\ q(y) \leftarrow B_2 \\ p(x) \leftarrow q(y), C \end{array}&\quad \quad \text{ into }\quad \quad&\begin{array}{l} p(x) \leftarrow B_1, C \\ p(x) \leftarrow B_2, C \end{array} \end{aligned}$$

(8)

To define this transformation precisely, we will use the notation $\phi |_{\iota }$ to mean the sub-formula of $\phi$ at syntactic position $\iota$ and $\phi [\psi ]_{\iota }$ to mean $\phi$ with $\psi$ substituted at syntactic position $\iota$. Now suppose we have two NNF clauses $C_1 = H_1 \leftarrow B_1$ and $C_2 = p(\mathbf {x}) \leftarrow B_2$ such that for some syntactic position $\iota$ in $B_1$, $B_1|_{\iota } = p(\mathbf {t})$. Assume (without loss of generality) that the variables occurring in $C_1$ and $C_2$ are disjoint. The resolvent of $C_1$ and $C_2$ at position $\iota$ is $H_1\leftarrow B_1[B_2\sigma ]_{\iota }$, where $\sigma$ maps $\mathbf {x}$ to $\mathbf {t}_i$. We denote this $C_1\langle C_2 \rangle _{\iota }$. The unfolding of $C_2$ in $C_1$ is $C_1\langle C_2\rangle _{\iota _1}\cdots \langle C_2\rangle _{\iota _k}$ where $\iota _1\ldots \iota _K$ are the positions in $B_1$ of the form $p(\mathbf {t})$. That is, unfolding means simultaneously resolving all occurrences of p.

The unfold transformation on p replaces each clause $C_1$ with the set of clauses obtained by unfolding all the p-clauses in $C_1$. The unfold transformation is a very frequently used pre-processing rule and we will use it later on in Sect. 4.3. It simplifies the set of clauses but does not change the search space for symbolic models. As we will see in many cases, we can use the tool of Craig interpolation [22] to characterize model preservation.

Proposition 9

The unfold transformation preserves $\mathcal {A}$-definable models if $\mathcal {A}$ admits interpolation.

Proof

Take for instance a symbolic model that contains the definition $p(x) := \varphi$ and satisfies the clauses on the right of (8) together with other clauses. Assume that the symbolic model also contains definitions $r_1(x) := \psi _1, \ldots , r_m(x) := \psi _m$ corresponding to other uninterpreted predicate symbols in $B_1, B_2, C$ and in other clauses. Then $((B_1 \vee B_2) \rightarrow (C \rightarrow p(x)))[\varphi /p,\psi _1/r_1, \ldots , \psi _m/r_m]$ is valid and we can assume the two sides of the implication only share the variable y. From our assumptions, there is an interpolant q(y).

We can do a little better than this in the case where there is exactly one p-clause $C: p(\mathbf {x}) \leftarrow B$. We say the reinforced resolvent of C with respect to clause $H \leftarrow B'$ at position $\iota$ (under the same conditions as above) is $H \leftarrow B'[p(\mathbf {t}) \wedge B\sigma ]_{\iota }$. Instead of replacing the predicate $p(\mathbf {t})$ with its definition, we conjoin it with the definition. This is valid when there is exactly one p-clause. In this case the original clauses and the reinforced clauses have the same initial models (which can be seen by unfolding once the corresponding recursive definition for p). Reinforced resolution induces a corresponding notion of reinforced unfolding. The reinforced unfold transformation on p applies only if there is exactly one p-clause. It replaces each clause C with the clause obtained by reinforced unfolding the unique p-clause in C. As an example:

$$\begin{aligned} \begin{array}{l} p(y) \leftarrow B \\ q(x) \leftarrow p(y), \phi \end{array}&\quad \quad \text{ unfolds } \text{ into }\quad \quad&\begin{array}{l} p(y) \leftarrow B \\ q(x) \leftarrow p(y), B, \phi \end{array} \end{aligned}$$

(9)

Proposition 10

The reinforced unfold transformation preserves $\mathcal {A}$-definable models if $\mathcal {A}$ admits interpolation.

Proof

Consider the example of (9), and suppose we have a solution $\mathcal {I}$ for the unfolded system (the right-hand side). Let $p'(y)$ be an interpolant for the valid implication $B\mathcal {I} \rightarrow (p(y) \wedge \phi \rightarrow q(x))\mathcal {I}$. Taking the conjunction of $p'$ with $\mathcal {I}(p)$, we obtain a solution for the original (left-hand side) system. This construction can be generalized to any number of reinforced resolutions on p by using the conjunction of all the interpolants (but only under the assumption that there is just one p-clause).

The fold transformation takes a rule $q(x) \leftarrow B$ and replaces B everywhere in other rules by q(x). For example it takes a system of the form:

$$\begin{aligned} \begin{array}{l} q(x) \leftarrow B\\ p(x) \leftarrow B, C \\ r(x) \leftarrow B, C' \end{array}&\quad \quad \text{ into }\quad \quad&\begin{array}{l} q(x) \leftarrow B\\ p(x) \leftarrow q(x), C \\ r(x) \leftarrow q(x), C' \end{array} \end{aligned}$$

(10)

To create opportunities for the fold transformation, rules for simplification and creating new definitions should also be used. For example, the rule $q(x) \leftarrow B$ is introduced for a fresh predicate q when there are multiple occurrences of B in the existing Horn clauses.

Remark 3

The fold/unfold transformations do not refer to goal, sub-goals or fact clauses. Thus, they can be applied to simplify and solve Horn clauses independent of top-down and bottom-up strategies.

K -induction and Reinforced Unfold. K-induction [64] is a powerful technique to prove invariants. It exploits the fact that many invariants become inductive when they are checked across more than one step. To establish that an invariant $safe$ is 2-inductive for a transition system with initial state $init$ and transition $step$ it suffices to show:

$$\begin{aligned} init (\mathbf {v})\rightarrow & {} safe (\mathbf {v}) \nonumber \\ init (\mathbf {v}) \wedge step (\mathbf {v},\mathbf {v}')\rightarrow & {} safe (\mathbf {v}') \\ safe (\mathbf {v}) \wedge step (\mathbf {v},\mathbf {v}') \wedge safe (\mathbf {v}') \wedge step (\mathbf {v}',\mathbf {v}'')\rightarrow & {} safe (\mathbf {v}'') \nonumber \end{aligned}$$

(11)

Formally, 2-induction can be seen as simply applying the reinforced unfold transformation on $safe$. That is, in NNF we have:

$$\begin{aligned} safe (\mathbf {v}') \leftarrow init (\mathbf {v}') \vee ( safe (\mathbf {v}) \wedge step (\mathbf {v},\mathbf {v}')) \end{aligned}$$

which unfolds to:

$$\begin{aligned} safe (\mathbf {v}'') \leftarrow init (\mathbf {v}'') \vee ( safe (\mathbf {v'}) \wedge ( init (\mathbf {v}') \vee ( safe (\mathbf {v}) \wedge step (\mathbf {v},\mathbf {v}'))\wedge step (\mathbf {v'},\mathbf {v}''))) \end{aligned}$$

which is equivalent to the clauses above. We can achieve K-induction for arbitrary K by simply unfolding the original definition of $safe$ $K-1$ times in itself. Checking that any given predicate $\phi$ is K-inductive amounts to plugging it in for $safe$ and checking validity. Interestingly, given a certificate $\pi$ of K-induction of $\phi$ and feasible interpolation [58], the proof of Proposition 10 gives us a way to solve the original clause set. This gives us an ordinary safety invariant whose size is polynomial in $\pi$ (though for propositional logic it may be exponential in the size of the original problem and $\phi$).

4.3 A Program Transformation for Inlining Assertions

To improve the performance of software model checking tools Gurfinkel, Wei and Chechik [35] used a transformation called mixed semantics that eliminated call stacks from program locations with assertions. It is used also in Corral, as described by Lal and Qadeer [49], as a pre-processing technique that works with sequential and multi-threaded programs. The SeaHorn verification tool [34] uses this technique for transforming intermediary representations. In this way, the LLVM infrastructure can also leverage the transformed programs. The technique transforms a program into another program while preserving the set of assertions that are provable. We will here be giving a logical account for the transformation and recast it at the level of Horn clauses. We will use Horn clauses that are created from the ${\mathsf {ToHorn}}$ transformation and we will then use Horn clauses created from the error flag encoding. We show in both cases that call stacks around assertions can be eliminated, but the steps are different. They highlight a duality between the two translation techniques: Boogie inserts predicates to encode safe pre-conditions to procedures. SeaHorn generates predicates to encode unsafe post-conditions of procedures. Either transformation eliminates the safe pre-condition or the unsafe post-condition.

Optimizing ${{\mathbf {\mathsf{{ToHorn}}}}.}$ Recall the Horn clauses from Example 3 that were extracted from Fig. 2. The clauses are satisfiable if and only if:

$$\begin{aligned} \varphi _2(y)\leftarrow & {} init (x), \psi (x,z), \psi (z,y) \\ \varphi _1(y)\leftarrow & {} init (x), \psi (x,z_1), \psi (z_1,z), \psi (z,z_2), \psi (z_2, y) \end{aligned}$$

is true. There are two main issues with direct inlining: (1) the result of inlining can cause an exponential blowup, (2) generally, when a program uses recursion and loops, finite inlining is impossible.

As a sweet spot one can inline stacks down to assertions in order to create easier constraint systems. The transformation proposed in [35, 49] converts the original program into the program in Fig. 3.

Fig. 3.

Program with partially inlined procedures

It has the effect of replacing the original Horn clauses by the set

$$\begin{aligned} \varphi _1(y)\leftarrow & {} init (x), p(x,z), p(z, y) \\ \varphi _2(z) \wedge p_{pre}(z)\leftarrow & {} init (x), q(x,z_1), q(z_1,z) \nonumber \\ \varphi _2(y)\leftarrow & {} init (x), p(x,z), q(z,z_1), q(z_1,y) \nonumber \\ p_{pre}(x)\leftarrow & {} init (x)\nonumber \\ p(x,y)\leftarrow & {} p_{pre}(x), q(x,z), q(z,y), \varphi _2(y) \nonumber \\ q(x,y)\leftarrow & {} \psi (x,y)\nonumber \end{aligned}$$

(12)

Part of this transformation corresponds to simple inlining of the calling contexts, but the transformation has another effect that is not justified by resolution alone: The formula $\varphi _2(y)$ is used as an assumption in the second to last rule. The transformation that adds $\varphi _2$ as an assumption is justified by the following proposition:

Proposition 11

The following clauses are equivalent:

$$\begin{aligned} \begin{array}{lll} \varphi &{} \leftarrow &{} B \\ P &{} \leftarrow &{} B \end{array}&\quad \quad \quad \quad \begin{array}{lll} \varphi &{} \leftarrow &{} B \\ P &{} \leftarrow &{} B, \varphi \end{array} \end{aligned}$$

We could in fact have baked in this transformation already when generating Horn clauses by pretending that every assert is followed by a matching assume, or by defining:

$$\begin{aligned} wlp (\mathbf{assert}\ \varphi , Q):= & {} \varphi \wedge (\varphi \rightarrow Q) \end{aligned}$$

Furthermore, the clauses from our running example are equi-satisfiable to:

$$\begin{aligned} \varphi _1(y)\leftarrow & {} init (x), p(x,z), p(z, y) \\ \varphi _2(z)\leftarrow & {} init (x), q(x,z_1), q(z_1,z) \nonumber \\ \varphi _2(y)\leftarrow & {} init (x), p(x,z), q(z,z_1), q(z_1,y) \nonumber \\ p(x,y)\leftarrow & {} q(x,z), q(z,y), \varphi _2(y) \nonumber \\ q(x,y)\leftarrow & {} \psi (x,y)\nonumber \end{aligned}$$

(13)

These clauses don’t contain $p_{pre}$. The place where $p_{pre}$ was used is in the rule that defines p. To justify this transformation let us refer to a general set of Horn clauses $\varPi$, and

• Let $\mathcal {P}: C_1, C_2, \ldots$ be the clauses where P occurs negatively at least once.

• Let $\mathcal {R}: Q \leftarrow D_1, Q \leftarrow D_2, \ldots$ be the clauses where Q occurs positively and assume Q does not occur negatively in these clauses.

Proposition 12

Let $P \leftarrow Q \wedge B$ be a clause in $\varPi$. Then $\varPi$ is equivalent to $\{ P \leftarrow B \} \cup \varPi$ if the following condition holds: For every clause $C \in \mathcal {P}$ let $C'$ be the result of resolving all occurrences of P with $P \leftarrow Q \wedge B$, then there exists a sequence of resolvents for Q from $\mathcal {R}$, such that each resolvent subsumes $C'$.

The intuition is of course that each pre-condition can be discharged by considering the calling context. We skip the tedious proof and instead give an example tracing how the proposition applies.

Example 5

Consider the clause $q(x,y) \leftarrow q_{pre}(x), \psi (x,y)$ from (3). We wish to show that $q_{pre}(x)$ can be removed from the premise. Thus, take for example the clause $q_{pre}(z) \leftarrow p_{pre}(x), q(x,z)$ where q occurs negatively. Then resolving with q produces $C'$: $q_{pre}(z) \leftarrow p_{pre}(x), q_{pre}(x), \psi (x,y)$. The pre-condition is removed by resolving with $q_{pre}(x) \leftarrow p_{pre}(x)$, producing the subsuming clause $q_{pre}(z) \leftarrow p_{pre}(x), p_{pre}(x), \psi (x,y)$. A somewhat more involved example is the clause $p(x,y) \leftarrow p_{pre}(x), q(x,z), q(z,y)$. We will have to resolve against q in both positions. For the first resolvent, we can eliminate $q_{pre}$ as we did before. Resolving against the second occurrence of q produces

$$\begin{aligned} p(x,y) \leftarrow p_{pre}(x), q(x,z), q_{pre}(z), \psi (z,y). \end{aligned}$$

This time resolve with the clause $q_{pre}(z) \leftarrow p_{pre}(x), q(x,z)$ producing

$$\begin{aligned} p(x,y) \leftarrow p_{pre}(x), q(x,z), q(x',z), p_{pre}(x'), \psi (z,y), \end{aligned}$$

which is equivalent to $p(x,y) \leftarrow p_{pre}(x), q(x,z), \psi (z,y)$.

The resulting Horn clauses are easier to solve: the burden to solve for $p_{pre}$ has been removed, and the clauses that constrain P have been weakened with an additional assumption. However, similar to other transformations, we claim we can retrieve a solution for $p_{pre}$ if $\mathcal {A}$ admits interpolation.

Error Flag Specialization. We can arrive to the same result using specialization of the Horn clauses generated from Sect. 3.2 followed by inlining. The specialization step is to create fresh copies of clauses by grounding the values of the Booleans $e_{i}$ and $e_{o}$.

Consider the clauses from Example 4. We specialize the clauses with respect to $e_{i}, e_{o}$ by instantiating the clauses according to the four combinations of the $e_{i}, e_{o}$ arguments. This reduction could potentially cause an exponential increase in number of clauses, but we can do much better: neither $p(x,y,\top ,\bot )$ nor $q(x,y,\top ,\bot )$ are derivable. This reduces the number of instantiations significantly from exponential to at most a linear overhead in the size of the largest clause. To reduce clutter, let $p_{fail}(x,y)$ be shorthand for $p(x,y,\bot ,\top )$ and $p_{ok}(x,y)$ be shorthand for $p(x,y,\bot ,\bot )$.

$$\begin{aligned} \bot\leftarrow & {} main _{fail} \\ main _{fail}\leftarrow & {} init (x), p_{fail}(x,y) \nonumber \\ main _{fail}\leftarrow & {} init (x), p_{ok}(x,y), p_{fail}(y, z)\nonumber \\ main _{fail}\leftarrow & {} init (x), p_{ok}(x,y), p_{ok}(y, z), \lnot \varphi _1(y) \nonumber \\ p_{fail}(x,ret)\leftarrow & {} q_{fail}(x,z) \nonumber \\ p_{fail}(x,ret)\leftarrow & {} q_{ok}(x,z), q_{fail}(z, ret)\nonumber \\ p_{fail}(x,ret)\leftarrow & {} q_{ok}(x,z), q_{ok}(z, ret), \lnot \varphi _2(ret) \nonumber \\ p_{ok}(x,ret)\leftarrow & {} q_{ok}(x,z), q_{ok}(z, ret), \varphi _2(ret) \nonumber \\ q_{ok}(x,ret)\leftarrow & {} \psi (x, ret)\nonumber \end{aligned}$$

(14)

In the end we get by unfolding the post-conditions for failure $main _{fail}$, $p_{fail}$ and $q_{fail}$:

$$\begin{aligned} \bot\leftarrow & {} init (x), q_{ok}(x,z), q_{ok}(z,y), \lnot \varphi _2(y) \\ \bot\leftarrow & {} init (x), p_{ok}(x,y), q_{ok}(y,u), q_{ok}(u,z), \lnot \varphi _2(z) \nonumber \\ \bot\leftarrow & {} init (x), p_{ok}(x,y), p_{ok}(y, z), \lnot \varphi _1(y) \nonumber \\ p_{ok}(x,ret)\leftarrow & {} q_{ok}(x,z), q_{ok}(z, ret), \varphi _2(ret) \nonumber \\ q_{ok}(x,ret)\leftarrow & {} \psi (x, ret) \nonumber \end{aligned}$$

(15)

which are semantically the same clauses as (13).

5 Conclusions and Continuations

We have described a framework for checking properties of programs by checking satisfiability of (Horn) clauses. We described main approaches for mapping sequential programs into Horn clauses and some main techniques for transforming Horn clauses. We demonstrated how many concepts developed in symbolic model checking can be phrased in terms of Horn clause solving. There are many extensions we did not describe here, and some are the focus of active research. Let us briefly mention a few areas here.

Games. Winning strategies in infinite games use alternations between least and greatest fixed-points. Horn clauses are insufficient and instead [9] encodes games using EHC, which by Proposition 5 amounts to solving general universally quantified formulas.

Theories. We left the assertion language $\mathcal {A}$ mostly unspecified. Current Horn clause solvers are mainly tuned for real and linear integer arithmetic and Boolean domains, but several other domains are highly desirable, including strings, bit-vectors, arrays, algebraic data-types, theories with quantifiers (EPR, the Bernays Schoenfinkel class). In general $\mathcal {A}$ can be defined over a set of templates or syntactically as formulas over a grammar for a limited language. For example, the sub-language of arithmetic where each inequality has two variables with coefficients $\pm 1$ is amenable to specialized solving. Finally, one can also treat separation logic as a theory [56].

Consequences and Abstraction Interpretation In CLP. While the strongest set of consequences from a set of Horn clauses is a least fixed-point over $\mathcal {A}$, one can use abstract domains to over-approximate the set of consequences. Thus, given a set of Horn clauses $\varPi$ over assertion language $\mathcal {A}$ compute the strongest consequences over assertion language $\mathcal {A'} \subseteq \mathcal {A}$.

Classification. There are several special cases of Horn clauses that can be solved using dedicated algorithms [63]. An example of “easier” clauses is linear Horn clauses that only contain at most one uninterpreted predicate in the bodies. Naturally, recursion-free Horn clauses can be solved whenever $\mathcal {A}$ is decidable. Horn clauses obtained from QBF problems with large blocks of quantified variables are solved more efficiently if one realizes that clauses can be rewritten corresponding to re-ordering variables.

Higher-Order Programs. The interpreter approach for assigning meanings to programs can be extended to closures in a straight-forward way. Closures encode function pointers and state and they can be encoded when $\mathcal {A}$ supports algebraic data-types [13]. This allows establishing properties of functional programs where all closures are defined within the program. The more general setting was given a custom proof system in [31], and modern approaches to proving properties of higher-order rewriting systems use a finite state abstraction as higher-order Boolean programs [59]. A different approach extracts Horn clauses from refinement based type systems for higher-order programs [44, 62].

Beyond $\mathcal {A}$ -definable Satisfiability. Our emphasis on $\mathcal {A}$-definable models is partially biased based on the methods developed by the authors, but note that methods based on superposition, infinite descent and fold/unfold can establish satisfiability of Horn clauses without producing a $\mathcal {A}$-definable model. Some other clausal transformation techniques we have not described are based on accelerating transitive relations [1, 27, 39].

Aggregates and Optimality. Suppose we would like to say that a program has at most a $2\cdot n$ reachable states for a parameter n. We can capture and solve such constraints by introducing cardinality operators that summarize the number of reachable states. Note that upper bounds constraints on cardinalities preserve least fixed-points: If there is a solution not exceeding a bound, then any conjunction of solutions also will not exceed a bound. Lower-bound constraints, on the other hand, are more subtle to capture. Rybalchenko et al. use a symbolic version of Barvinok’s algorithm [7] to solve cardinality constraints. Instead of proving bounds, we may also be interested in finding solutions that optimize objective functions.

We would like to thank Dejan Jovanovic and two peer reviewers for extensive feedback on an earlier version of the manuscript.