key: cord-0049776-uds9l987
authors: Kobayashi, Naoki; Fedyukovich, Grigory; Gupta, Aarti
title: Fold/Unfold Transformations for Fixpoint Logic
date: 2020-03-13
journal: Tools and Algorithms for the Construction and Analysis of Systems
DOI: 10.1007/978-3-030-45237-7_12
sha: 530e233c2361463c6fa0c8ec9c0ba6adad50e897
doc_id: 49776
cord_uid: uds9l987

Fixpoint logics have recently been drawing attention as common foundations for automated program verification. We formalize fold/unfold transformations for fixpoint logic formulas and show how they can be used to enhance a recent fixpoint-logic approach to automated program verification, including automated verification of relational and temporal properties. We have implemented the transformations in a tool and confirmed its effectiveness through experiments.

A wide range of program properties can be verified by reducing to satisfiability/validity in a fixpoint logic [3-6, 18, 20, 22, 23, 29, 35] . In this paper, we build on top of MuArith, a first-order logic with least/greatest fixpoint operators and integer arithmetic, recently proposed by Kobayashi et al. [22] . It offers a powerful tool to handle the full class of modal µ-calculus properties of while-programs (imperative programs with loops but without general recursion). In contrast, earlier studies on temporal program verification require different methods for each subclass of the modal µ-calculus properties, such as LTL [12, 16, 28] , CTL [2, 3, 13, 34] , and CTL * [11] . The recent program verifier based on MuArith [22] is effective in practice, i.e., by exploiting general-purpose solvers for Satisfiability Modulo Theories (SMT) and Constrained Horn Clauses (CHC), it can outperform tools designed specifically for CTL verification of C programs [13] .

Despite these promising results, the generality of the fixpoint logic approach come at a cost. Since fixpoint logic formulas obtained by reduction from various verification problems often involve nested fixpoint operators, it could be challenging to check the validity of these formulas automatically. To enhance the capability of fixpoint logic provers, in this paper, we propose novel fold/unfold transformations and prove their correctness. These transformations are generally used to simplify relational verification, and in particular, to reduce the number of recurrences used in the program (or a set of programs) under analysis. Originally proposed for logic programming [8, 19, 32] , they have been recently adopted for determining the satisfiability of CHC [15, 26] and allow discovery of relational invariants for a pair of loopy (or recursive) programs, as opposed to invariants within each individual program. Our transformations can be regarded as extensions of such transformations for a fixpoint logic, where quantifiers and arbitrarily nested least/greatest fixpoint operators are allowed.

We also present a procedure that seeks a way to apply the proposed fold/ unfold transformations efficiently. Besides non-determinism in the choice of which fixpoint formulas to unfold, our "fold" operation replaces a formula φ with P (where P is the predicate defined by P △ = φ) and requires various reasoning to convert the current goal formula to a form E [φ] , where the form of E can be more complex than in the case of fold/unfold transformations for logic programming or CHC.

We have implemented the transformations and integrated them with the program verifier Mu2CHC [22] based on MuArith. We considered a number of examples of MuArith formulas which include formulas obtained from program verification problems for checking relational and temporal properties. Our new transformations allowed Mu2CHC to solve these formulas, which would not be doable otherwise.

To sum up, our contributions are: (i) a formalization of fold/unfold transformations for a fixpoint logic and proofs of their soundness, (ii) demonstration of the usefulness of the proposed transformations for verification of relational and temporal properties of programs, and (iii) a concrete procedure for automated transformation and its implementation and experiments.

The rest of this paper is structured as follows. Section 2 reviews the definition of the first-order fixpoint logic MuArith [22] , and reductions from program verification problems to validity checking in MuArith. Section 3 formalizes our transformations and proves their correctness. Section 4 shows applications of our transformations to verification of relational and temporal properties of recursive programs. Section 5 reports an implementation and experimental results. Section 6 discusses related work and Section 7 concludes the paper.

We review the first-order fixpoint logic MuArith [22] in this section. MuArith is a variation of Mu-Arithmetic studied by Lubarsky [25] and Bradfield [7] , obtained by replacing natural numbers with integers.

The set of (propositional) formulas, ranged over by ϕ, is defined in the following grammar.

a (arithmetic expressions) ::= n | x | a 1 + a 2 | a 1 − a 2

The metavariable ϕ represents a proposition, and P denotes a predicate on (a tuple of) integers. We write ⊤ for 0 ≥ 0 and ⊥ for 0 ≥ 1. In examples, we may also use other relational symbols such as > and =. The meta-variable x denotes an integer, and the meta-variable X (k) denotes a k-ary first-order predicate variable. We write ar(X (k) ) for the arity of the predicate variable X (k) , i.e., k; we often omit the superscript (k) and just write X for a predicate variable. The predicate µX (k) (x 1 , . . . , x k ).ϕ (resp. νX (k) (x 1 , . . . , x k ).ϕ) denotes the least (resp. greatest) predicate X such that X(x 1 , . . . , x k ) equals ϕ.

We write FV(ϕ) for the set of free (predicate and integer) variables in ϕ; ∀x, ∃x, µX (k) , νX (k) , and λx are binders. We sometimes write x for a sequence of variables x 1 , . . . , x k . We often write ϕ and X for the De Morgan dual of a formula ϕ and a predicate variable X, respectively. For example,

Here, X is a predicate variable, so the righthand side is α-equivalent to νX(x).x = 0 ∧ X(x − 1). The overline for X is used to indicate that it corresponds to the dual of X in the original formula µX(x).x = 0 ∨ X(x − 1).

In this subsection, we define the formal semantics of formulas. Let Z be the set of integers, and

where Z k denotes the set of tuples consisting of k integers). We define the partial order ⊑ k on D k by:

f ⊑ k g ⇔ ∀n 1 , . . . , n k ∈ Z.f (n 1 , . . . , n k ) ⊑ B g(n 1 , . . . , n k ).

Note that (D k , ⊑ k ) is a complete lattice, with λx 1 . · · · λx k .⊥ B and λx 1 . · · · λx k .⊤ B as the least and greatest elements. We write ⊥ k and ⊤ k for λx 1 . · · · λx k .⊥ B and λx 1 . · · · λx k .⊤ B , respectively. We also write ⊓ (k) (resp., ⊔ (k) ) for the greatest lower (resp., least upper) bound with respect to ⊑ k . We often omit k and B and just write ⊤, ⊥, ⊑, ⊓, ⊔, etc.. We often identify B and D 0 = Z 0 → B. We write D k → D ℓ for the set of monotonic functions from D k to D ℓ .

We write Env for the set of functions that map each integer variable to an integer, and each k-ary predicate variable to an element of D k . For a formula ϕ (resp., a predicate P and an expression a) and an environment ρ ∈ Env such that FV(ϕ) ⊆ dom(Env) (resp., FV(P ) ⊆ dom(Env) and FV(a) ⊆ dom(Env)), Fig. 1 defines the semantics · ρ of ϕ (resp., P and a), where for a mono-

When ϕ and P are closed (i.e., do not contain free variables), we just write ϕ and P for ϕ ∅ and P ∅ respectively. By abuse of notation, we often write ϕ ⊒ ψ if ϕ ρ ⊒ ψ ρ for any (valid) environment ρ such that FV(ϕ)∪FV(ψ) ⊆ dom(ρ), and ϕ ≡ ψ if ϕ ρ = ψ ρ; similarly for predicates. For example, ∃z.(x > z ∧ z > y) ≡ (x > y + 1) ⊒ (x > y + 2).

. . , a k ) ρ = P ρ( a1 ρ, . . . , a k ρ) 

. Since for any m, F m (λx ∈ Z.⊥) = λn ∈ Z.0 ≤ n ≤ m − 1, we have LFP (1) (F ) = λn ∈ Z.0 ≤ n (here, ≤ denotes the semantic relation on integers). In contrast, νX(x).x = 0 ∨ X(x − 1) ∅ = GFP (1) (F ) = λn ∈ Z.⊤. ⊓ ⊔

Various verification problems for first-order recursive programs can be reduced to validity of MuArith formulas. We refer the reader to [22] for a general reduction schema from temporal properties to MuArith formulas. However, as shown in this subsection, some formulas require additional handling that motivates the need for new transformations to be presented in Section 3. Consider the following functional program (written in the syntax of OCaml) that multiplies two numbers.

let rec mult(x, y) = if y=0 then 0 else x + mult(x,y-1)

Then, the ternary relation Mult (x, y, r) that expresses "mult(x, y) terminates and returns r" is expressed as the following MuArith formula:

µMult (x, y, r).(y = 0 ∧ r = 0) ∨ ∃s.(y = 0 ∧ r = x + s ∧ Mult (x, y − 1, s)).

This lets us express a partial correctness property "if P (x, y) holds and mult(x, y) terminates and returns r, then Q(x, y, r) holds" by: ∀x, y, r.P (x, y)∧Mult (x, y, r) ⇒ Q(x, y, r). It can further be rewritten to the following MuArith formula:

where P and Mult are respectively De Morgan duals of P and Mult ; Mult can be expressed by:

The total correctness "if P (x, y), then mult(x, y) terminates and returns r, such that Q(x, y, r)" can be expressed by: ∀x, y.P (x, y) ⇒ ∃r.Mult (x, y, r) ∧ Q(x, y, r), which is equivalent to the MuArith formula:

As a special case, the termination property "if y ≥ 0 then mult(x, y) terminates" can be expressed by:

We can also express relational properties of programs such as the equivalence of two programs. Let us consider another implementation of multiplication: let mult2(x,y) = let rec multacc(x,y,a) = if y=0 then a else multacc(x,y-1,x+a) in multacc(x,y,0)

Then predicate Multacc(x, y, a, r) which represents "multacc(x, y, a) terminates and returns r" can be expressed by:

Thus, the equivalence of mult and mult2 can be expressed by: ∀x, y, r.Mult (x, y, r) ⇔ Multacc(x, y, 0, r), which can be expressed by the conjunction of the MuArith formulas:

where Multacc is the De Morgan dual of Multacc, defined analogously to Mult .

Motivation. Kobayashi et al. [22] presented a method for proving the validity of MuArith formulas. It can prove formula (1) valid: since there are neither µ nor ∃, it is reducible to the problem of satisfiability of CHC [4] . However, the method is not powerful enough on formulas (2) and (3) for termination and program equivalence, respectively. It first tries to eliminate existential quantifiers and µformulas, so that the resulting formula can be reduced to the satisfiability of CHC. But it fails when the witness of an existential quantifier (i.e., r such that ∃r.ϕ) is not bounded by a linear expression, e.g., the witness for ∃r is a non-linear expression x × y in the case of (2). This is unfortunate, as methods specialized on proving program termination, e.g. [18] , can easily prove the termination of program mult. Thus, in order to exploit the advantage of the uniform approach to program verification based on MuArith, we need to strengthen the method for proving MuArith formulas.

We introduce additional definitions on formulas, which will be used later in our formalization of fold/unfold-like transformations. A (k, ℓ)-context (or, just a context) is an expression obtained from an ℓ-ary predicate by replacing a k-ary predicate variable with [ ] (in other words, a context is a predicate that may contain [ ] as a special predicate variable). For a context C and a predicate P (that does not contain free occurrences of variables bound in C), we write C[P ] for the predicate obtained by replacing [ ] with P . For example,

and λf.f ∧ g is both continuous and co-continuous for any ϕ ∈ D 0 . In contrast, λf.∃x.f (x) ∈ D 1 → D 0 is continuous but not cocontinuous; 4 λf.∀x.f (x) ∈ D 1 → D 0 is co-continuous but not continuous. We say that a context C is continuous if its semantics, i.e., λf. C[X] {X → f } is; analogously for co-continuity.

The following lemma (which follows immediately from the definition) provides a syntactic condition that is sufficient for the co-continuity of a context. Lemma 1. Let C be a (k, ℓ)-context. If C can be generated by the following syntax, then C is co-continuous. 5

The syntax and semantics of MuArith was defined based on hierarchical fixpoint equations (HES) in [22] . The above semantics is equivalent to that of [22] , modulo the standard conversions between fixpoint formulas and HES. 5 Here, for the sake of simplicity, we mix the syntax of contexts that yield predicates and propositions.

In this section, we present new fold/unfold-like transformations for MuArith, to enhance the power of MuArith validity checkers. We first informally review fold/unfold transformations for logic programming and explain what kind of transformation we wish to apply to MuArith formulas in Section 3.1. We then prove theorems that justify such transformations in Sections 3.2 and 3.3.

Revisiting Fold/Unfold Transformations for Logic Programming The original concept [32] is presented in the following example, where each recurrence is represented by a CHC (i.e., an implication involving uninterpreted predicates Even and Odd ).

We wish to prove that ⊥ ⇐ Even(x), Odd (x). Many of the existing CHC solvers, such as HoICE [9] and Z3 [24] , fail to prove it as they do not handle the divisibility constraints well. After defining a new predicate EvenOdd as EvenOdd (x) ⇐ Even(x), Odd (x) and unfolding Even, we obtain the following new CHCs.

By unfolding Odd (x) in the first CHC, its body becomes inconsistent. By unfolding Odd (x) in the second CHC, we obtain the following new CHCs.

By unfolding Even(x − 2), the body of the first CHC becomes inconsistent. Now, the part "Odd (x − 2), Even(x − 2)" in the second CHC matches the definition of EvenOdd , so we can "fold" it and obtain the following new CHC.

The least solution for EvenOdd is λx.⊥, hence we have now obtained ⊥ ⇐ Even(x), Odd (x) without synthesizing interpretations of Even and Odd over the divisibility constraints.

Transformations for MuArith. The above example can be reformulated in MuArith. Predicates Even and Odd are expressed as follows.

µEven(x).

µOdd (x).

We wish to prove that Even(x)∧Odd (x) is inconsistent, i.e. ∀x.Even(x)∨Odd (x) is valid where Even and Odd are:

, which can be rewritten as follows.

Based on this, we wish to replace Y with νY (x).x ≤ 0 ∨ Y (x − 2); then the validity of ∀x.Y (x) would follow immediately. As we will see later in Section 3.3, this transformation is indeed sound. Intuitively, the above transformation works as follows. Given a formula C[X], which contains a fixpoint formula X defined by the equation

, which serves as a new definition clause for Y . We wish to apply this kind of transformation not only to ν-only formulas like above, but also to formulas involving µ and quantifiers, as discussed below.

Recall formula (2) ≡ y = 0 ∨ (y = 0 ∧ X(x, y − 1)).

As justified later in Section 3.2, we can then replace X with µX(x, y).y = 0∨(y = 0 ∧ X(x, y − 1)). We are then left with formula ∀x, y.y < 0 ∨ X(x, y), which can then be proved valid by Mu2CHC [22] , the existing MuArith validity checker. Let us also recall a generalized version of formula (3):

∀x, y, a, r.Mult (x, y, r) ∨ Multacc(x, y, a, r + a), which contains µ and ν. Let Y (x, y, a, r) y, a, r + a) . Then, we have:

As justified in Section 3.3, we can replace Y with νY (x, y, a, r).(y = 0 ∨ Y (x, y − 1, x + a, r − x)), giving us ∀x, y, a, r.Y (x, y, a, r) immediately.

Although the above transformations are sound, the soundness of fold/unfold transformations for MuArith is delicate in general. For example, consider formula ∃x.x ≥ y ∧ X(x, y), where:

It is obviously false since there exists no x that satisfies

Based on this, one may be tempted to replace Y with νY (y).Y (y + 1) ≡ λy.⊤, but that is obviously wrong.

In the next two subsections, we present theorems that justify all the transformations above except the last (invalid) one.

In this subsection, we prove a theorem that enables the replacement of a predicate of the form C[µX.D[X]] with one of the form µY.E[Y ] and applies it to justify the transformation for ∃r.Mult (x, y, r) discussed in the previous subsection. The corresponding transformation for ν-formulas is discussed in the next subsection. The theorem is stated as follows. The theorem follows easily from the definition of the semantics of the least fixpoint operator.

Since

To see how the theorem above enables fold/unfold-like transformations, suppose that we wish to prove a formula of the form Y ≡ C[µX(

Thus, by the theorem, it suffices to prove µY ( y).E[Y ]( y), which is obtained by "folding" C[µX.D[X]( x)] to Y . Note that the theorem guarantees only that the transformation provides an underapproximation of the original predicate. A stronger condition is required for the equivalence; see Corollary 1 given later. Note also that finding an appropriate context E may not be easy in general; we discuss how to mechanically find E in Section 5. Then, for any ternary predicate X, we have:

By Theorem 1, we have C[D[Mult ]] ⊒ µY (x, y).y = 0 ∨ (y = 0 ∧ Y (x, y)). Thus, the goal ∀x, y.y < 0 ∨ ∃r.Mult (x, y, r) has been reduced to:

∀x, y.y < 0 ∨ (µY (x, y).y = 0 ∨ (y = 0 ∧ Y (x, y)))(x, y), which can be proved valid by Mu2CHC. ⊓ ⊔

We now prove a theorem that allows us to replace a predicate of the form

. It is similar to Theorem 1, but requires more conditions. Recall Lemma 1, which provides a sufficient syntactic condition for the co-continuity. Proof. For F ∈ D k → D k , f ∈ D k and an ordinal γ, we define F γ (⊤ (k) ) inductively by: F 0 (⊤ (k) ) = ⊤ (k) , F γ+1 (⊤ (k) ) = F (F γ (⊤ (k) )), and F γ (⊤ (k) ) = ⊓ γ ′ <γ F γ ′ (⊤ (k) ) if γ is a limit ordinal. By abuse of notation, we write D γ [⊤ (k) ] for D γ (⊤ (k) ) if D is a (k, k)-context. Since there exists an ordinal γ such that νX.

] holds for any ordinal γ, by transfinite induction on γ.

The base case where γ = 0 follows immediately from the first condition. If γ is a successor ordinal γ ′ + 1, then

Here, we have used the induction hypothesis in the second inequality. If γ is a limit ordinal, then we have:

Here we have used the co-continuity in the second inequality. We have thus y, a, r) .

They satisfy all the three conditions of Theorem 2. In particular, for any ternary predicate X, we have

based on the corresponding transformations shown in Section 3.1. We have thus ∀x, y, a, r.Mult (x, y, r) ∨ Multacc(x, y, a, r + a) ⊒ ∀x, y, a, r. (νY (x, y, a, r) y, a, r) , and the righthand side can be proved to be valid by Mu2CHC. 

In this section, we give more examples to demonstrate the utility of our transformations for relational/temporal property verification of recursive programs.

Below we discuss an example which is beyond the reach for state-of-the-art CHC solvers (see e.g., [33] , the end of Section 5).

Example 5. Consider the goal ∀x, y, z, r.(Mult (x + y, z, r) ⇒ ∃s, t.Mult (x, z, s) ∧ Mult(y, z, t) ∧ r = s + t), which is equivalent to: ∀x, y, z, r.(Mult (x + y, z, r) ∨ ∃s, t.(Mult (x, z, s) ∧ Mult (y, z, t) ∧ r = s + t)),

where Mult and Mult are as given in Section 2.3. The following contexts C, D, and E satisfy the following three conditions of Theorem 2. y, z, r) .[ ](x + y, z, r) ∨ ∃s, t. (Mult (x, z, s) ∧ Mult(y, z, t) 

By Theorem 2, we have C[Mult ] ⊒ νY (x, y, z, r).E[Y ](x, y, z, r) ≡ λ(x, y, z, r).⊤. We have thus proved that ∀x, y, z, r.C[Mult](x, y, z, r) (i.e., ∀x, y, z, r.(Mult(x + y, z, r) ⇒ ∃s, t.Mult(x, z, s) ∧ Mult(y, z, t) ∧ r = s + t)) is valid.

⊓ ⊔

Here we give an example of proving a liveness property of a recursive program by using our transformation. The example is a variation of the example discussed in [22] , but it cannot be handled by their method for proving MuArith formulas. 

Here, Sum is the De Morgan dual of Sum. The validity of this formula cannot be proved by Mu2CHC due to the existential quantifier. Note that Mu2CHC replaces each existential quantifier ∃x.ϕ with a bounded quantifier ∃x ≤ a.ϕ, and a must be a linear expression. In the example above, x is not linearly bounded by n. To remove the existential quantifier, let 

Input: Formula Φ of the form X(f (x, y)) ∨ Y (g(x, y)), where X and Y are predicates defined by αX , αY ∈ {µ, ν}.

] holds, we can apply Theorem 1 to underapproximate ∃x.Sum(n, x) by µX(n).n = 0 ∨ (n = 0 ∧ X(n − 1)). Therefore, the goal has been reduced to Repeat ′ (0) where

which can be proved valid by Mu2CHC automatically. ⊓ ⊔

In this section, we first present an algorithm for our transformation and then outline its implementation and report on experimental results.

Theorems 1 and 2 given in Section 3 state sufficient conditions for our fold/unfold transformation to be sound. In this subsection, we discuss how to systematically apply the theorems and how to find a context E.

To make it easy to find E, we restrict input formulas of our transformations to those of the form X(f (x, y)) ∨ Y (g(x, y)), X(f (x, y)) ∧ Y (g(x, y)), and ∃y.X(f (x, y)), where X and Y are predicates defined by fixpoint operators, and f (x, y) and g(x, y) denote (possibly sequences of) terms that may contain free variables x and y. For the sake of simplicity, we assume here that the definitions for X and Y are independent; X cannot be obtained by unfolding Y , and vice versa. Transformations for more complex formulas like the one in Example 5 can be achieved by repeatedly applying the transformations for smaller contexts.

The transformation algorithm for disjunctive formulas is shown in Algorithm 1. It takes as input a formula Φ = X(f (x, y)) ∨ Y (g(x, y)) and outputs an underapproximation Φ ′ of Φ. It can take [ ](f (x, y)) ∨ Y (g(x, y)) or X(f (x, y)) ∨ [ ](g(x, y)) as the context C and apply Theorem 2 if X or Y is Algorithm 2: Fold/unfold for ∃ Input: Formula Φ of the form ∃y.X(f (x, y)), where X is a predicate defined by µ or ν.

defined by ν, and Theorem 1 otherwise (line 1). On line 2, the algorithm unfolds X and Y 6 and then normalizes the resulting formula to a conjunctive normal form (CNF), where quantified formulas are treated as atomic. It then applies the "fold" transformation to each conjunct ψ i . To this end, for each ψ i that contains X(s 1 ) ∨ Y (s 2 ), the algorithm finds terms t 1 and t 2 such that X(s 1 ) ∨ Y (s 2 ) ≡ X(f (t 1 , t 2 )) ∨ Y (g(t 1 , t 2 )); this is achieved by solving the unification constraints s 1 ≡ f (x ′ , y ′ ) and s 2 ≡ g(x ′ , y ′ ) modulo arithmetic theories, where x ′ and y ′ are treated as variables but x and y are treated as constants. Finally, the algorithm replaces X(s 1 ) ∨ Y (s 2 ) with Z(t 1 , t 2 ), where Z(x, y) is a new predicate that corresponds to X(f (x, y)) ∨ Y (g(x, y)).

We omit the transformation algorithm for conjunctive formulas since it is similar to the case above, except that the new predicate Z is bound by µ (note that condition (i) of Theorem 2 may not be satisfied), and that it converts the unfolded formula to a disjunctive normal form (DNF), instead of CNF.

The algorithm for existential formulas is shown in Algorithm 2. It unfolds X, normalizes existential quantifiers, and obtains a DNF. In the normalization of existential quantifiers, it moves existential quantifiers inwards (by using, e.g., the law ∃x.(ψ 1 ∨ ψ 2 ) ≡ (∃x.ψ 1 ) ∨ (∃x.ψ 2 )) and eliminates them as much as possible (by using, e.g., the equality-based quantifier elimination). For each disjunct ψ i of the form (∃z.X(s)) ∧ ψ ′ i , it finds t x and t z , such that f (t x , y) ≡ [t z /z]s (again, by performing unification modulo arithmetic theories), and replaces the disjunct with Z(t x ) ∧ ψ ′ i . Here, Z(t x ) corresponds to ∃y.X(f (t x , y)), and t z serves as a witness for X(f (t x , y)) ⇒ ∃z.X(s).

We have implemented the transformation in a tool called MuFolder based on the algorithms discussed above, on top of the AdtInd theorem prover [37] , using its routines for pattern-matching, normalization, and simplification. For the implication checks, MUnfold uses the Z3 SMT solver [27] . MuFolder can be tested at https://www.kb.is.s.u-tokyo.ac.jp/ ∼ koba/mu/. 

νZ(x).x = 0 ∨ Z(x − 2) 4 Mult(x + y, z, r) ∨ ∃s.Mult(x, z, s) νZ(x, y, z, r).z = 0 ∨ Z(x, y, z − 1, r − (x + y)) 5 Mult(x + y, z, r)∨ ∃s1, s2.

νZ(x, y, z, r).z = 0 ∨ Z(x, y, z − 1, r − (x + y)) Mult(x, z, s1) ∧ Mult(y, z, s2) ∧ r = s1 + s2 6 Mult(2x + 3y, z, r) ∨ ∃s1, s2.

νZ(x, y, z, r).z = 0∨ Mult(x, z, s1) ∧ Mult(y, z, s2) ∧ r = 2s1 + 3s2 z = 0 ∧ Z(x, y, z − 1, r − (2x + 3y)) 7 Mult(x, y, r) ∨ Mult(x, y, r)

νZ(x, y, r).y = 0 ∨ y = 0 ∧ Z(x, y − 1, r − x) 8 Mult(x, y, r) ∨ MultAcc(x, y, a, r + a) νZ(x, y, a, r).y = 0∨ y = 0 ∧ Z(x, y − 1, x + a, r − x) 9 ∃r.Mult(x, y, r)

µZ(x, y).y = 0 ∨ y = 0 ∧ Z(x, y − 1) 10 P lus(x + y, z, r) ∨ ∃s.P lus(x, z, s) νZ(x, y, z, r).z = 0 ∨ Z(x, y, z − 1, r − 1) 11 P lus(4x − 3y, z, r) ∨ ∃s1, s2.

νZ(x, y, z, r).z = 0 ∨ Z(x, y, z − 1, r − 1) P lus(x, z, s1) ∧ P lus(y, z, s2) ∧ r = 4s1 − 3s2 12 ∃r.Sum(x, r) µZ(x).

We have evaluated MuFolder on several benchmarks outlined in Table 1 . These benchmarks include formulas obtained from the relational and temporal verification properties; some of which have been taken from the benchmark set for Unno et al.'s induction-based CHC solver [33] and modified to include both µ and ν. We have confirmed that all the benchmark problems can be solved in our approach within a few seconds. To our knowledge, except the formulas 7, 8 (for which the method of [33] can be used) and 10,11 (for which Mu2CHC works), Mu2CHC (without our transformation) or the existing CHC solvers cannot directly prove the validity of the formulas. Note that formula 12 comes from Example 6. The combination of the transformation with Mu2CHC enables fully automated verification of Example 6.

As already mentioned, fold/unfold transformations have been originally proposed for logic programming [32] , and later extended for CHC (a.k.a. constraint logic programs) [1, 17] . Those transformations have originally been proposed to speed up program execution, but recently, Mordvinov and Fedyukovich [26] and De Angelis et al. [15] shown that related transformations are also useful in the context of verification based on CHC solving. Those transformations correspond to the transformation for the ν-only fragment of MuArith. 7 Our transformation can thus be considered an extension of fold/unfold-like transformations to MuArith, which allows alternations of least/greatest fixpoints. Sato [31] studied an extension of fold/unfold transformations for a first-order logic, where negations and quantifiers are allowed in clause bodies; thus, some mixtures of least/greatest fixpoints are allowed. The correctness of his transformation is, however, based on a three-valued logic, hence different from MuArith. The correctness of most of the transformations mentioned above is guaranteed by some syntactic conditions, while our transformation is based on semantic conditions. Unno et al. [33] proposed a method for automatically solving CHC problems by using induction. Their method is based on a tailor-made proof system; hence it is difficult to integrate the method with other CHC or MuArith solvers (in fact, that disadvantage motivated the above-mentioned work of De Angelis et al. [15] ). Their method slightly goes beyond the CHC satisfiability (or the ν-only fragment of MuArith) but cannot deal with complex combinations of least/greatest fixpoints and quantifiers (like ∀x, y, z, r.(Mult(x + y, z, r) ⇒ ∃s, t.Mult(x, z, s) ∧ Mult(y, z, t) ∧ r = s + t), discussed in Section 4).

As mentioned in Section 1, fixpoint logic-based approaches to program verification (including CHC-based ones) have been drawing attention. Kobayashi et al. [22, 23, 35] have shown that temporal property verification of (higher-order) programs can be reduced to the validity checking of (higher-order) fixpoint logic formulas. They proposed a concrete method for checking validity of first-order fixpoint formulas and implemented a validity checking tool Mu2CHC. As discussed already, our transformations can be used to improve the capability of Mu2CHC. Another thread of work on a fixpoint logic-based approach to system verification is that of Parameterized Boolean Equation Systems (PBES) [21] . Actually, MuArith may be considered an instance of PBES, where data are restricted to integers. Groote, Willemse, and others [10, 14, 21, 30, 36] studied applications of PBES to verification of infinite state systems, and devised various techniques for solving PBES. To our knowledge, however, they have not studied fold/unfold transformations for PBES.

We have formalized fold/unfold-like transformations for a fixpoint logic, and shown that they are useful for verification of relational/temporal properties of recursive programs. We have implemented the transformations, and shown their effectiveness through experiments.

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Transforming constraint logic programs

Slayer: Memory safety for systems-level code

Solving existentially quantified horn clauses

Horn clause solvers for program verification

Program verification as satisfiability modulo theories

Higher-order program verification as satisfiability modulo theories with algebraic data-types

Fixpoint alternation and the game quantifier

A transformation system for developing recursive programs

Hoice: An ice-based non-linear horn clause solver

Equivalence checking for infinite systems using parameterized boolean equation systems

On automation of CTL* verification for infinite-state systems

Making prophecies with decision predicates

Reasoning about nondeterminism in programs

Proof graphs for parameterised boolean equation systems

Solving horn clauses on inductive data types without induction

Fairness modulo theory: A new approach to LTL software model checking

Transformations of CLP modules

Syntax-guided termination analysis

Unfold/fold transformations of logic programs. In: Computational Logic -Essays in Honor of Alan Robinson

Synthesizing software verifiers from proof rules

Parameterised boolean equation systems

Temporal verification of programs via first-order fixpoint logic

Higher-order program verification via HFL model checking

Smt-based model checking for recursive programs

µ-definable sets of integers

Synchronizing constrained horn clauses

Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference

Temporal verification of higher-order functional programs

A fixpoint logic and dependent effects for temporal property verification

Invariants for parameterised boolean equation systems

Equivalence-preserving first-order unfold/fold transformation systems

Unfold/fold transformation of logic programs

Automating induction for solving horn clauses

Abstract interpretation of CTL properties

Reduction from branching-time property verification of higher-order programs to HFL validity checking

Evidence extraction from parameterised boolean equation systems

Lemma Synthesis for Automating Induction over Algebraic Data Types

Acknowledgments. We would like to thank anonymous referees for useful comments, especially for bringing the work on PBES to our attention. This work was supported in part by the University of Tokyo-Princeton Strategic Partnership Grant, JSPS KAKENHI Grant Number JP15H05706, and NSF (USA) award FMitF 1837030.