checking may actually be considered an extension of HORS model checking in the following sense. HORS model checking algorithms [21,32] usually consist of two phases, one for computing a kind of higher-order "procedure summaries" in the form of variable profiles [32] or intersection types [21], and the other for nested least/greatest fixpoint computations. Our reduction from program verification to extended HFL model checking (the reduction given in Sect. 7, in particular) can be regarded as an extension of the first phase to deal with infinite data domains, where the problem for the second phase is expressed in the form of extended HFL model checking: see [23] for more details.

The rest of this paper is structured as follows. Section 2 introduces HFL extended with integer predicates and defines the HFL model checking problem. Section 3 informally demonstrates some examples of reductions from program verification problems to HFL model checking. Section 4 introduces a functional language used to formally discuss the reductions in later sections. Sections 5, 6, and 7 consider may/must-reachability, trace properties, and temporal properties respectively, and present (sound and complete) reductions from verification of those properties to HFL model checking. Section 8 discusses related work, and Sect. 9 concludes the paper. Proofs are found in an extended version [23].

### **2 (Extended) HFL**

In this section, we introduce an extension of higher-order modal fixpoint logic (HFL) [42] with integer predicates (which we call HFL**Z**; we often drop the subscript and write HFL, as in Sect. 1), and define the HFL**Z** model checking problem. The set of integers can actually be replaced by another infinite set X of data (like the set of natural numbers or the set of finite trees) to yield HFLX.

### **2.1 Syntax**

For a map f, we write *dom*(f) and *codom*(f) for the domain and codomain of f respectively. We write **Z** for the set of integers, ranged over by the metavariable n below. We assume a set **Pred** of primitive predicates on integers, ranged over by p. We write arity(p) for the arity of p. We assume that **Pred** contains standard integer predicates such as = and <, and also assume that, for each predicate p ∈ **Pred**, there also exists a predicate ¬p ∈ **Pred** such that, for any integers n1,...,nk, p(n1,...,nk) holds if and only if ¬p(n1,...,nk) does not hold; thus, ¬p(n1,...,nk) should be parsed as (¬p)(n1,...,nk), but can semantically be interpreted as ¬(p(n1,...,nk)).

The syntax of HFL**Z** *formulas* is given by:

$$\begin{array}{c} \varphi \text{ (fermulas)} ::= n \mid \varphi\_1 \text{ op } \varphi\_2 \mid \mathsf{true} \mid \mathsf{false} \mid p(\varphi\_1, \dots, \varphi\_k) \mid \varphi\_1 \lor \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \land \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_1 \mid \varphi\_2 \mid \varphi\_$$

Here, op ranges over a set of binary operations on integers, such as +, and X ranges over a denumerable set of variables. We have extended the original HFL [42] with integer expressions (n and ϕ1 op ϕ2), and atomic formulas p(ϕ1,...,ϕk) on integers (here, the arguments of integer operations or predicates will be restricted to integer expressions by the type system introduced below). Following [19], we have omitted negations, as any formula can be transformed to an equivalent negation-free formula [30].

We explain the meaning of each formula informally; the formal semantics is given in Sect. 2.2. Like modal μ-calculus [10,25], each formula expresses a property of a labeled transition system. The first line of the syntax of formulas consists of the standard constructs of predicate logics. On the second line, as in the standard modal μ-calculus, aϕ means that there exists an a-labeled transition to a state that satisfies ϕ. The formula [a]ϕ means that after any alabeled transition, ϕ is satisfied. The formulas μXτ .ϕ and νXτ .ϕ represent the least and greatest fixpoints respectively (the least and greatest X that X = ϕ) respectively; unlike the modal μ-calculus, X may range over not only propositional variables but also higher-order predicate variables (of type τ ). The λabstractions λX :σ.ϕ and applications ϕ1 ϕ2 are used to manipulate higher-order predicates. We often omit type annotations in μXτ .ϕ, νXτ .ϕ and λX : σ.ϕ, and just write μX.ϕ, νX.ϕ and λX.ϕ.

*Example 1.* Consider ϕab ϕ where ϕab = μX•→•.λY : •.Y ∨ a(X(bY )). We can expand the formula as follows:

$$\begin{split} \varphi\_{\mathbf{a}\mathbf{b}}\varphi &= (\lambda Y.\bullet.Y \lor \langle \mathbf{a} \rangle (\varphi\_{\mathbf{a}\mathbf{b}}(\langle \mathbf{b} \rangle Y)))\varphi = \varphi \lor \langle \mathbf{a} \rangle (\varphi\_{\mathbf{a}\mathbf{b}}(\langle \mathbf{b} \rangle \varphi))) \\ &= \varphi \lor \langle \mathbf{a} \rangle (\langle \mathbf{b} \rangle \varphi \lor \langle \mathbf{a} \rangle (\varphi\_{\mathbf{a}\mathbf{b}}(\langle \mathbf{b} \rangle \langle \mathbf{b} \rangle \varphi))) = \cdots \end{split}$$

and obtain ϕ ∨ (abϕ) ∨ (aabbϕ) ∨···. Thus, the formula means that there is a transition sequence of the form anbn for some n ≥ 0 that leads to a state satisfying ϕ.

Following [19], we exclude out unmeaningful formulas such as (a**true**)+1 by using a simple type system. The types •, int, and σ → τ describe propositions, integers, and (monotonic) functions from σ to τ , respectively. Note that the integer type int may occur only in an argument position; this restriction is required to ensure that least and greatest fixpoints are well-defined. The typing rules for formulas are given in Fig. 2. In the figure, Δ denotes a type environment, which is a finite map from variables to (extended) types. Below we consider only well-typed formulas.

### **2.2 Semantics and HFLZ Model Checking**

We now define the formal semantics of HFL**Z** formulas.  We write s1 a−→ s2 when (s1, a, s2) ∈ −→.

For an LTS L = (U, A, −→, sinit) and an extended type σ, we define the partially ordered set (DL,σ, L,σ) inductively by:

$$\begin{array}{lll} \mathcal{D}\_{\mathsf{L},\bullet} = 2^{U} & \sqsubseteq\_{\mathsf{L},\bullet} \sqcap\_{\bullet} = \subseteq & \mathcal{D}\_{\mathsf{L},\mathsf{int}} = \mathbf{Z} & \sqsubseteq\_{\mathsf{L},\mathsf{int}} = \{(n,n) \mid n \in \mathbf{Z}\} \\ \mathcal{D}\_{\mathsf{L},\sigma \to \tau} = \{f \in \mathcal{D}\_{\mathsf{L},\sigma} \to \mathcal{D}\_{\mathsf{L},\tau} \mid \forall x, y. (x \sqsubseteq\_{\mathsf{L},\sigma} y \Rightarrow f \ x \sqsubseteq\_{\mathsf{L},\tau} f \, y)\} \\ \sqsubseteq\_{\mathsf{L},\sigma \to \tau} = \{(f,g) \mid \forall x \in \mathcal{D}\_{\mathsf{L},\sigma}.f(x) \sqsubseteq\_{\mathsf{L},\tau} g(x)\} \end{array}$$

**Fig. 2.** Typing rules for HFL**Z** formulas

Note that (DL,τ , L,τ ) forms a complete lattice (but (DL,int, L,int) does not). We write ⊥L,τ and L,τ for the least and greatest elements of DL,τ (which are λx. - ∅ and λx.U- ) respectively. We sometimes omit the subscript L below. Let -ΔL be the set of functions (called *valuations*) that maps X to an element of DL,σ for each X : σ ∈ Δ. For an HFL formula ϕ such that Δ H ϕ : σ, we define -Δ H ϕ : σL as a map from -ΔL to Dσ, by induction on the derivation4 of Δ H ϕ : σ, as follows.

4 Note that the derivation of each judgment Δ -H ϕ : σ is unique if there is any.

Here, op denotes the binary function on integers represented by op and p denotes the k-ary relation on integers represented by p. The least/greatest fixpoint operators **lfp**L,τ and **gfp**L,τ are defined by **lfp**L,τ (f) = L,τ {x ∈ DL,τ | f(x) L,τ x} and **gfp**L,τ (f) = L,τ {x ∈ DL,τ | x L,τ f(x)}. Here, L,τ and L,τ respectively denote the least upper bound and the greatest lower bound with respect to L,τ . We often omit the subscript L and write -Δ H ϕ : σ for -Δ H ϕ : σL. For a closed formula, i.e., a formula well-typed under the empty type environment ∅, we often write ϕL or just ϕ for -∅ H ϕ : σL(∅).

*Example 2.* For the LTS L*file* in Fig. 1, we have:

$$\begin{aligned} & \left[ \nu X^{\bullet}. (\langle \mathtt{close} \rangle \mathtt{true} \land \langle \mathtt{read} \rangle X) \right] = \\ & \mathbf{gfp}\_{\mathtt{L},\bullet} (\lambda x \in \mathcal{D}\_{\mathtt{L},\bullet} \left[ X : \bullet \vdash \langle \mathtt{close} \rangle \mathtt{true} \land \langle \mathtt{read} \rangle X : \bullet \right] (\{ X \mapsto x \})) = \{ q\_{0} \}. \end{aligned}$$

In fact, x = {q0}∈DL,• satisfies the equation: -X : •close**true** ∧ readX : •L({X → x}) = x, and x = {q0}∈DL,• is the greatest such element.

Consider the following LTS L1:

and ϕab (c**true**) where ϕab is the one introduced in Example 1. Then, ϕab (c**true**)L1 = {q0, q2}.

**Definition 1 (HFLZ model checking).** *For a closed formula* ϕ *of type* •*, we write* L, s |= ϕ *if* s ∈ ϕL*, and write* L |= ϕ *if* sinit ∈ ϕL*.* HFL**Z** model checking *is the problem of, given* L *and* ϕ*, deciding whether* L |= ϕ *holds.*

The HFL**Z** model checking problem is *un*decidable, due to the presence of integers; in fact, the semantic domain DL,σ is not finite for σ that contains int. The undecidability is obtained as a corollary of the soundness and completeness of the reduction from the may-reachability problem to HFL model checking discussed in Sect. 5. For the fragment of pure HFL (i.e., HFL**Z** without integers, which we write HFL∅ below), the model checking problem is decidable [42].

The *order* of an HFL**Z** model checking problem L ? |= ϕ is the highest order of types of subformulas of ϕ, where the order of a type is defined by: order(•) = order(int) = 0 and order(σ → τ ) = max(order(σ)+1, order(τ )). The complexity of order-k HFL∅ model checking is k-EXPTIME complete [1], but polynomial time in the size of HFL formulas under the assumption that the other parameters (the size of LTS and the largest size of types used in formulas) are fixed [19].

*Remark 1.* Though we do not have quantifiers on integers as primitives, we can encode them using fixpoint operators. Given a formula ϕ : int → •, we can express ∃x : int.ϕ(x) and ∀x : int.ϕ(x) by (μXint→•.λx : int.ϕ(x) ∨ X(x − 1) ∨ X(x + 1))0 and (νXint→•.λx : int.ϕ(x) ∧ X(x − 1) ∧ X(x + 1))0 respectively.

### **2.3 HES**

As in [19], we often write an HFL**Z** formula as a sequence of fixpoint equations, called a *hierarchical equation system* (HES).

**Definition 2.** *An (extended)* hierarchical equation system *(HES) is a pair* (E, ϕ) *where* E *is a sequence of fixpoint equations, of the form:* Xτ1 1 =α1 ϕ1; ··· ; Xτn n =αn ϕn*, where* αi ∈ {μ, ν}*. We assume that* X1 : τ1,...,Xn : τn H ϕi : τi *holds for each* i ∈ {1,...,n}*, and that* ϕ1,...,ϕn, ϕ *do not contain any fixpoint operators.*

The HES Φ = (E, ϕ) represents the HFL**Z** formula *toHFL*(E, ϕ) defined inductively by: *toHFL*(, ϕ) = ϕ and *toHFL*(E; Xτ =α ϕ , ϕ) = *toHFL*([αXτ .ϕ /X]E, [αXτ .ϕ /X]ϕ). Conversely, every HFL**Z** formula can be easily converted to an equivalent HES. In the rest of the paper, we often represent an HFL**Z** formula in the form of HES, and just call it an HFL**Z** formula. We write -Φ for *toHFL*(Φ). An HES (Xτ1 1 =α1 ϕ1; ··· ; Xτn n =αn ϕn, ϕ) can be normalized to (Xτ0 0 =ν ϕ; Xτ1 1 =α1 ϕ1; ··· ; Xτn n =αn ϕn, X0) where τ0 is the type of ϕ. Thus, we sometimes call just a sequence of equations Xτ0 0 =ν ϕ; Xτ1 1 =α1 ϕ1; ··· ; Xτn n =αn ϕn an HES, with the understanding that "the main formula" is the first variable X0. Also, we often write Xτ x1 ··· xk =α ϕ for the equation Xτ =α λx1. ··· λxk.ϕ. We often omit type annotations and just write X =α ϕ for Xτ =α ϕ.

*Example 3.* The formula νX.μY.bX∨aY (which means that the current state has a transition sequence of the form (a∗b)ω) is expressed as the following HES:

$$((X =\_\nu Y; Y =\_\mu \langle \mathbf{b} \rangle X \lor \langle \mathbf{a} \rangle Y), \quad X).$$

### **3 Warming Up**

To help readers get more familiar with HFL**Z** and the idea of reductions, we give here some variations of the examples of verification of file-accessing programs in Sect. 1, which are instances of the "resource usage verification problem" [15]. General reductions will be discussed in Sects. 5, 6 and 7, after the target language is set up in Sect. 4.

Consider the following OCaml-like program, which uses exceptions.

```
let readex x = read x; (if * then () else raise Eof) in
let rec f x = readex x; f x in
```
let d = open\_in "foo" in try f d with Eof -> close d Here, \* represents a non-deterministic boolean value. The function readex reads the file pointer x, and then non-deterministically raises an end-of-file (Eof) exception. The main expression (on the third line) first opens file "foo", calls f to read the file repeatedly, and closes the file upon an end-of-file exception. Suppose, as in the example of Sect. 1, we wish to verify that the file "foo" is accessed following the protocol in Fig. 1.

First, we can remove exceptions by representing an exception handler as a special continuation [6]:

```
let readex x h k = read x; (if * then k() else h()) in
let rec f x h k = readex x h (fun _ -> f x h k) in
let d = open_in "foo" in f d (fun _ -> close d) (fun _ -> ())
```
Here, we have added to each function two parameters h and k, which represent an exception handler and a (normal) continuation respectively.

Let Φ be (E, F **true** (λr.close**true**) (λr.**true**)) where E is:

> *Readex* xhk =ν read(k **true** ∧ h **true**); F xhk =ν *Readex* x h (λr.F x h k).

Here, we have just replaced read/close operations with the modal operators read and close, non-deterministic choice with a logical conjunction, and the unit value ( ) with **true**. Then, L*file* |= Φ if and only if the program performs only valid accesses to the file (e.g., it does not access the file after a close operation), where L*file* is the LTS shown in Fig. 1. The correctness of the reduction can be informally understood by observing that there is a close correspondence between reductions of the program and those of the HFL formula above, and when the program reaches a read command read x, the corresponding formula is of the form read···, meaning that the read operation is valid in the current state; a similar condition holds also for close operations. We will present a general translation and prove its correctness in Sect. 6.

Let us consider another example, which uses integers:

```
let rec f y x k = if y=0 then (close x; k())
                  else (read x; f (y-1) x k) in
let d = open_in "foo" in f n d (fun _ -> ())
```
Here, n is an integer constant. The function f reads x y times, and then calls the continuation k. Let L *file* be the LTS obtained by adding to L*file* a new state q2 and the transition q1 end −→ q2 (which intuitively means that a program is allowed to terminate in the state q1), and let Φ be (E ,F n **true** (λr.end**true**)) where E is:

$$F\ y\ x\ k = \mu\ (y = 0 \Rightarrow \langle \mathtt{c1ose} \rangle (k\mathtt{true})) \land (y \neq 0 \Rightarrow \langle \mathtt{read} \rangle (F\ (y - 1)\ x\ k)).$$

Here, p(ϕ1,...,ϕk) ⇒ ϕ is an abbreviation of ¬p(ϕ1,...,ϕk) ∨ ϕ. Then, L *file* |= Φ if and only if (i) the program performs only valid accesses to the file, (ii) it eventually terminates, and (iii) the file is closed when the program terminates. Notice the use of μ instead of ν above; by using μ, we can express liveness properties. The property L *file* |= Φ indeed holds for n ≥ 0, but not for n < 0. In fact, F nxk is equivalent to **false** for n < 0, and readnclose(k **true**) for n ≥ 0.

### **4 Target Language**

This section sets up, as the target of program verification, a call-by-name5 higherorder functional language extended with events. The language is essentially the same as the one used by Watanabe et al. [43] for discussing fair non-termination.

### **4.1 Syntax and Typing**

We assume a finite set **Ev** of names called *events*, ranged over by a, and a denumerable set of variables, ranged over by x, y, . . .. Events are used to express temporal properties of programs. We write x- (t, resp.) for a sequence of variables (terms, resp.), and write |x-| for the length of the sequence. A *program* is a pair (D, t) consisting of a set D of function definitions {f1 xt1,...,fn x-

1 = n = tn} and a term t. The set of *terms*, ranged over by t, is defined by:

$$t \colon= \begin{pmatrix} \\ \end{pmatrix} \mid x \mid n \mid t\_1 \text{ op } t\_2 \mid \textbf{event} \; a; t \mid \textbf{if} \; p(t\_1', \dots, t\_k') \text{ then } t\_1 \text{ else } t\_2.$$

Here, n and p range over the sets of integers and integer predicates as in HFL formulas. The expression **event** a;t raises an event a, and then evaluates t. Events are used to encode program properties of interest. For example, an assertion **assert**(b) can be expressed as **if** b **then** ( ) **else** (**event** fail; Ω), where fail is an event that expresses an assertion failure and Ω is a non-terminating term. If program termination is of interest, one can insert "**event** end" to every termination point and check whether an end event occurs. The expression t1t2 evaluates t1 or t2 in a non-deterministic manner; it can be used to model, e.g., unknown inputs from an environment. We use the meta-variable P for programs. When P = (D, t) with D = {f1 x-1 = t1,...,fn xn = tn}, we write **funs**(P) for {f1,...,fn} (i.e., the set of function names defined in P). Using λ-abstractions, we sometimes write f = λx.t for the function definition f x- = t. We also regard D as a map from function names to terms, and write *dom*(D) for {f1,...,fn} and D(fi) for λxi.ti.

Any program (D, t) can be normalized to (D ∪ {**main** = t}, **main**) where **main** is a name for the "main" function. We sometimes write just D for a program (D, **main**), with the understanding that D contains a definition of **main**.

We restrict the syntax of expressions using a type system. The set of *simple types*, ranged over by κ, is defined by:

$$\kappa ::= \star \mid \eta \to \kappa \qquad\qquad \eta ::= \kappa \mid \mathsf{int}.$$

The types , int, and η → κ describe the unit value, integers, and functions from η to κ respectively. Note that int is allowed to occur only in argument

5 Call-by-value programs can be handled by applying the CPS transformation before applying the reductions to HFL model checking.

positions. We defer typing rules to [23], as they are standard, except that we require that the righthand side of each function definition must have type ; this restriction, as well as the restriction that int occurs only in argument positions, does not lose generality, as those conditions can be ensured by applying CPS transformation. We consider below only well-typed programs.

#### **4.2 Operational Semantics**

We define the labeled transition relation t −→D t , where is either or an event name, as the least relation closed under the rules in Fig. 3. We implicitly assume that the program (D, t) is well-typed, and this assumption is maintained throughout reductions by the standard type preservation property. In the rules for if-expressions, t i represents the integer value denoted by t i; note that the well-typedness of (D, t) guarantees that t i must be arithmetic expressions consisting of integers and integer operations; thus, t i is well defined. We often omit the subscript D when it is clear from the context. We write t 1···k −→ ∗ D t if t 1 −→D ··· k −→D t . Here, is treated as an empty sequence; thus, for example, we write t ab −→∗ D t if t a−→D −→D b −→D −→D t .

$$\begin{array}{cc} \textbf{Event} \ a; t \stackrel{a}{\longrightarrow}\_{D} t & \frac{f\widetilde{\boldsymbol{x}} = \boldsymbol{u} \in \boldsymbol{D} \qquad | \widetilde{\boldsymbol{x}}| = |\widetilde{\boldsymbol{t}}|}{f \ \widetilde{\boldsymbol{t}} \stackrel{\boldsymbol{\epsilon}}{\longrightarrow}\_{D} [\widetilde{\boldsymbol{t}}/\widetilde{\boldsymbol{x}}] \boldsymbol{u}} & \frac{([\boldsymbol{t}\_{1}^{\prime}], \ldots, \underbrace{[\boldsymbol{t}\_{k}^{\prime}]}) \in [\boldsymbol{p}]}{\textbf{if} \ \boldsymbol{p}(t\_{1}^{\prime}, \ldots, \boldsymbol{t}\_{k}^{\prime}) \ \textbf{then} \ t\_{1} \ \mathtt{else} \ t\_{2} \stackrel{\boldsymbol{\epsilon}}{\longrightarrow}\_{D} t\_{1}} \\\\ & \frac{\boldsymbol{i} \in \{1, 2\}}{t\_{1} \Box t\_{2} \stackrel{\boldsymbol{\epsilon}}{\longrightarrow}\_{D} t\_{i}} & \frac{([\boldsymbol{t}\_{1}^{\prime}], \ldots, [\boldsymbol{t}\_{k}^{\prime}]) \notin [\boldsymbol{p}]}{\textbf{if} \ \boldsymbol{p}(t\_{1}^{\prime}, \ldots, \boldsymbol{t}\_{k}^{\prime}) \ \textbf{then} \ t\_{1} \ \mathtt{else} \ t\_{2} \stackrel{\boldsymbol{\epsilon}}{\longrightarrow}\_{D} t\_{2}} \end{array}$$

**Fig. 3.** Labeled transition semantics

For a program P = (D, t0), we define the set **Traces**(P)(⊆ **Ev**∗ ∪ **Ev**ω) of *traces* by:

$$\begin{split} \mathbf{Taxes}(D, t\_0) &= \{ \ell\_0 \cdots \ell\_{n-1} \in (\{\epsilon\} \cup \mathbf{Ev})^\* \mid \forall i \in \{0, \ldots, n-1\}. t\_i \stackrel{\ell\_i}{\longrightarrow}\_D t\_{i+1} \} \\ &\cup \{ \ell\_0 \ell\_1 \cdots \in (\{\epsilon\} \cup \mathbf{Ev})^{\omega} \mid \forall i \in \omega. t\_i \stackrel{\ell\_i}{\longrightarrow}\_D t\_{i+1} \}. \end{split}$$

Note that since the label is regarded as an empty sequence, 012 = aa if 0 = 2 = a and 1 = , and an element of ({} ∪ **Ev**)ω is regarded as that of **Ev**∗ ∪ **Ev**ω. We write **FinTraces**(P) and **InfTraces**(P) for **Traces**(P) ∩ **Ev**∗ and **Traces**(P) ∩ **Ev**ω respectively. The set of *full traces* **FullTraces**(D, t0)(⊆ **Ev**∗ ∪ **Ev**ω) is defined as:

$$\begin{split} \{\ell\_0 \cdots \ell\_{n-1} \in (\{\epsilon\} \cup \mathbf{Ev})^\* \mid t\_n = (\ ) \land \forall i \in \{0, \ldots, n-1\}. t\_i \xrightarrow{\ell\_i}\_{D} t\_{i+1} \} \\ \cup \{\ell\_0 \ell\_1 \cdots \in (\{\epsilon\} \cup \mathbf{Ev})^\omega \mid \forall i \in \omega. t\_i \xrightarrow{\ell\_i}\_{D} t\_{i+1} \}. \end{split}$$

*Example 4.* The last example in Sect. 1 is modeled as P*file* = (D, f ( )), where D = {f x = (**event** close; ( ))-(**event** read; **event** read; f x)}. We have:

**Traces**(P) = {readn | n ≥ 0}∪{read2nclose | n ≥ 0}∪{readω} **FinTraces**(P) = {readn | n ≥ 0}∪{read2nclose | n ≥ 0} **InfTraces**(P) = {readω} **FullTraces**(P) = {read2nclose | n ≥ 0}∪{readω}.

### **5 May/Must-Reachability Verification**

Here we consider the following problems:

Since we are interested in a particular event a, we restrict here the event set **Ev** to a singleton set of the form {a}. Then, the may-reachability is formalized as a ? ∈ **Traces**(P), whereas the must-reachability is formalized as "does every trace in **FullTraces**(P) contain a?" We encode both problems into the validity of HFL**Z** formulas (without any modal operators a or [a]), or the HFL**Z** model checking of those formulas against a trivial model (which consists of a single state without any transitions). Since our reductions are sound and complete, the characterizations of their negations –non-reachability and may-non-reachability– can also be obtained immediately. Although these are the simplest classes of properties among those discussed in Sects. 5, 6 and 7, they are already large enough to accommodate many program properties discussed in the literature, including lack of assertion failures/uncaught exceptions [22] (which can be characterized as non-reachability; recall the encoding of assertions in Sect. 4), termination [27,29] (characterized as must-reachability), and non-termination [26] (characterized as may-non-reachability).

### **5.1 May-Reachability**

As in the examples in Sect. 3, we translate a program to a formula that says "the program may raise an event a" in a compositional manner. For example, **event** a;t can be translated to **true** (since the event will surely be raised immediately), and t1t2 can be translated to t † 1 ∨ t † 2 where t † i is the result of the translation of ti (since only one of t1 and t2 needs to raise an event).

**Definition 3.** *Let* P = (D, t) *be a program.* ΦP,*may is the HES* (D†*may* , t†*may* )*, where* D†*may and* t †*may are defined by:* {f1 x-1 = t1,...,fn x-†*may* = f1 x-†*may* ; ··· ; fn xn =μ tn†*may*

$$\begin{array}{ll} \left( \begin{array}{l} f\_{1} \ \widetilde{x}\_{1} = t\_{1}, \ldots, f\_{n} \ \widetilde{x}\_{n} = t\_{n} \end{array} \right)^{\dagger\_{\text{may}}} = \left( f\_{1} \ \widetilde{x}\_{1} = \mu\_{1} \, t\_{1}^{\dagger\_{\text{may}}}; \cdots; f\_{n} \ \widetilde{x}\_{n} = \mu\_{n} \, t\_{n}^{\dagger\_{\text{may}}} \right) \\ \left( \begin{array}{l} \left( \right)^{\dagger\_{\text{may}}} = \text{false} \ \qquad x^{\dagger\_{\text{may}}} = x \ \qquad n^{\dagger\_{\text{may}}} = n \ \qquad \left( t\_{1} \ \text{op} \ t\_{2} \right)^{\dagger\_{\text{may}}} = t\_{1}^{\dagger\_{\text{may}}} \ \text{op} \ t\_{2} \, t^{\dagger\_{\text{may}}} \\ \text{(if } \ p(t\_{1}^{\dagger}, \ldots, t\_{k}^{\dagger}) \ \text{then } t\_{1} \ \text{else } t\_{2} \end{array} \right) = \\ \left( p(t\_{1}^{\dagger} \, ^{\dagger\_{\text{may}}}, \ldots, t\_{k}^{\dagger} \ ^{\dagger\_{\text{may}}}) \land t\_{1}^{\dagger\_{\text{may}}} \right) \vee \left( \neg p(t\_{1}^{\dagger} \, ^{\dagger\_{\text{may}}}, \ldots, t\_{k}^{\dagger} \ ^{\dagger\_{\text{may}}}) \wedge t\_{2}^{\dagger\_{\text{may}}} \right) \\ \left( \begin{array}{l} \mathbf{e} \text{'} \ \mathbf{t} \text{ or} \ \mathbf{t} \end{array} \right) \end{array}$$

Note that, in the definition of D†*may* , the order of function definitions in D does not matter (i.e., the resulting HES is unique up to the semantic equality), since all the fixpoint variables are bound by μ.

*Example 5.* Consider the program:

$$P\_{loop} = (\{loop\ x = loop\ x\}, loop(\textbf{event\ a}; ())).$$

It is translated to the HES Φ*loop* = (*loop* x =μ *loop* x, *loop*(**true**)). Since *loop* ≡ μ*loop*.λx.*loop* x is equivalent to λx.**false**, Φ*loop* is equivalent to **false**. In fact, P*loop* never raises an event a (recall that our language is call-by-name).

*Example 6.* Consider the program P*sum* = (D*sum*, **main**) where D*sum* is:

$$\begin{array}{l} \textbf{main} = \textit{sum} \ n \ (\lambda r. \textbf{assert}(r \ge n)) \\\quad \textit{sum } x \ k = \textbf{if} \ x = 0 \ \textbf{then} \ k \ 0 \ \textbf{else} \ sum \ (x - 1) \ (\lambda r. k(x + r)) \end{array}$$

Here, n is some integer constant, and **assert**(b) is the macro introduced in Sect. 4. We have used λ-abstractions for the sake of readability. The function *sum* is a CPS version of a function that computes the summation of integers from 1 to x. The main function computes the sum r =1+ ··· + n, and asserts r ≥ n. It is translated to the HES ΦP2,*may* = (E*sum*, **main**) where E*sum* is:

\*\*main =\*\*\_
um  $n$  ( $\lambda r. ( $r \ge n \land \mathtt{false}$ ) \lor ( $r < n \land \mathtt{true}$ ));

sum x  $k =\_\mu (x = 0 \land k \, 0) \lor (x \ne 0 \land \displaystyle sum \; (x - 1) \; (\lambda r. k(x + r))).$ $

Here, n is treated as a constant. Since the shape of the formula does not depend on the value of n, the property "an assertion failure may occur for some n" can be expressed by ∃n.ΦP2,*may*.

The following theorem states that ΦP,*may* is a complete characterization of the may-reachability of P.

**Theorem 1.** *Let* P *be a program. Then,* a ∈ **Traces**(P) *if and only if* L0 |= ΦP,*may for* L0 = ({s }, ∅, ∅, s )*.*

A proof of the theorem above is found in [23]. We only provide an outline. We first show the theorem for recursion-free programs and then lift it to arbitrary programs by using the continuity of functions represented in the fixpoint-free fragment of HFL**Z** formulas. To show the theorem for recursion-free programs, we define the reduction relation t −→D t by: fx- = u ∈ D |x-| = |-

and by using one continuity of n functions represented in one xpom-neent of HFLz formulas. To show the theorem for recursion-free programs define the reduction relation  $t \longrightarrow\_D t'$  by:

 $\frac{f\widetilde{x} = u \in D \qquad |\widetilde{x}| = |\widetilde{t}|}{E[f\,\widetilde{t}] \longrightarrow\_D E[\widetilde{[t/\widetilde{x}]u]}]} \quad \frac{([t'\_1], \ldots, [t'\_k]) \in [p]}{E[\widetilde{\text{if}}\, p(t'\_1, \ldots, t'\_k) \text{ then } t\_1 \text{ else } t\_2] \longrightarrow\_D E[t\_1]}$
 $\frac{([t'\_1], \ldots, [t'\_k]) \notin [p]}{(t'\_1 = t'\_1) \downarrow 1 \quad \star \quad 1 \quad \star \quad 1 \quad \star \quad 1 \quad \neg \quad 1}$

E[**if** p(t 1,...,t k) **then** t1 **else** t2] −→D E[t2]

Here, E ranges over the set of evaluation contexts given by E:: = [ ] | Et | t-E | **event** a; E. The reduction relation differs from the labeled transition relation given in Sect. 4, in that and **event** a; ··· are not eliminated. By the definition of the translation, the theorem holds for programs in normal form (with respect to the reduction relation), and the semantics of translated HFL formulas is preserved by the reduction relation; thus the theorem holds for recursion-free programs, as they are strongly normalizing.

### **5.2 Must-Reachability**

The characterization of must-reachability can be obtained by an easy modification of the characterization of may-reachability: we just need to replace branches with logical conjunction.

**Definition 4.** *Let* P = (D, t) *be a program.* ΦP,*must is the HES* (D†*must*, t†*must*)*, where* D†*must and* t †*must are defined by:* {f1 x-1 = t1,...,fn x-†*must* = f1 x-†*must*; ··· ; fn xn =μ tn†*must*

n = tn} 1 =μ t1 ( )†*must* = **false** x†*must* = x n†*must* = n (t1 op t2) †*must* = t1 †*must* op t2 †*must* (**if** p(t 1,...,t k) **then** t1 **else** t2) †*must* = (p(t 1 †*must*,...,t k †*must*) ⇒ t1 †*must*) ∧ (¬p(t 1 †*must*,...,t k †*must*) ⇒ t2 †*must*) (**event** a;t) †*must* = **true** (t1t2) †*must* = t1 †*must*t2 †*must* (t1t2) †*must* = t1 †*must* ∧ t2 †*must*.

*Here,* p(ϕ1,...,ϕk) ⇒ ϕ *is a shorthand for* ¬p(ϕ1,...,ϕk) ∨ ϕ*.*

*Example 7.* Consider Ploop = (D, loop m n) where D is:

$$\begin{array}{l} \textbf{1oop} \ x \ y = \textbf{if} \ x \leq 0 \lor y \leq 0 \ \textbf{then} \ (\textbf{event} \ \textbf{end}; \ ()) \\\quad \texttt{else} \ (\textbf{1oop} \ (x-1) \ (y\*y)) \square (\textbf{1oop} \ x \ (y-1)) \end{array}$$

Here, the event end is used to signal the termination of the program. The function loop non-deterministically updates the values of x and y until either x or y becomes non-positive. The must-termination of the program is characterized by ΦPloop,*must* = (E, loop m n) where E is:

$$\begin{array}{c} \mathsf{Top}\ x\ y =\_{\mu} (x \leq 0 \lor y \leq 0 \Rightarrow \mathsf{true})\\ \land (\neg(x \leq 0 \lor y \leq 0) \Rightarrow (\mathsf{Loop}\ (x-1)\ (y\*y)) \land (\mathsf{Loop}\ x\ (y-1))). \end{array}$$

We write **Must**a(P) if every π ∈ **FullTraces**(P) contains a. The following theorem, which can be proved in a manner similar to Theorem 1, guarantees that ΦP,*must* is indeed a sound and complete characterization of the must-reachability.

**Theorem 2.** *Let* P *be a program. Then, Must*a(P) *if and only if* L0 |= ΦP,*must for* L0 = ({s }, ∅, ∅, s )*.*

### **6 Trace Properties**

Here we consider the verification problem: "Given a (non-ω) regular language L and a program P, does *every* finite event sequence of P belong to L? (i.e. **FinTraces**(P) ? ⊆ L)" and reduce it to an HFL**Z** model checking problem. The verification of file-accessing programs considered in Sect. 3 may be considered an instance of the problem.

Here we assume that the language L is closed under the prefix operation; this does not lose generality because **FinTraces**(P) is also closed under the prefix operation. We write AL = (Q, Σ, δ, q0, F) for the minimal, deterministic automaton with no dead states (hence the transition function δ may be partial). Since L is prefix-closed and the automaton is minimal, w ∈ L if and only if ˆδ(q0, w) is defined (where ˆδ is defined by: ˆδ(q, ) = q and ˆδ(q, aw) = ˆδ(δ(q, a), w)). We use the corresponding LTS LL = (Q, Σ, {(q, a, q ) | δ(q, a) = q }, q0) as the model of the reduced HFL**Z** model checking problem.

Given the LTS LL above, whether an event sequence a1 ··· ak belongs to L can be expressed as LL ? |= a1···ak**true**. Whether all the event sequences in {aj,1 ··· aj,kj | j ∈ {1,...,n}} belong to L can be expressed as LL ? |= j∈{1,...,n}aj,1···aj,kj **true**. We can lift these translations for event sequences to the translation from a program (which can be considered a description of a set of event sequences) to an HFL**Z** formula, as follows. †*path* = n =ν tn†*path*

**Definition 5.** *Let* P = (D, t) *be a program.* ΦP,*path is the HES* (D†*path* , t†*path* )*, where* D†*path and* t †*path are defined by:* {f1 x-1 = t1,...,fn xf1 x-†*path* ; ··· ; fn x-

n = tn} 1 =ν t1 ( )†*path* = **true** x†*path* = x n†*path* = n (t1 op t2) †*path* = t1 †*path* op t2 †*path* (**if** p(t 1,...,t k) **then** t1 **else** t2) †*path* = (p(t 1 †*path* ,...,t k †*path* ) ⇒ t1 †*path* ) ∧ (¬p(t 1 †*path* ,...,t k †*path* ) ⇒ t2 †*path* ) (**event** a;t) †*path* = at †*path* (t1t2) †*path* = t1 †*path* t2 †*path* (t1t2) †*path* = t1 †*path* ∧ t2 †*path* .

*Example 8.* The last program discussed in Sect. 3 is modeled as P2 = (D2,f mg), where m is an integer constant and D2 consists of:

fyk = **if** y = 0 **then** (**event** close; k ( )) **else** (**event** read; f (y − 1) k) g r = **event** end;()

Here, we have modeled accesses to the file, and termination as events.  Then LL is L *file* in Sect. 3, and **FinTraces**(P2)⊆L can be verified by checking LL|=ΦP2,*path*.

6 Unlike in Sect. 3, the variables are bound by ν since we are not concerned with the termination property here.

**Theorem 3.** *Let* P *be a program and* L *be a regular, prefix-closed language. Then,* **FinTraces**(P) ⊆ L *if and only if* LL |= ΦP,*path.*

As in Sect. 5, we first prove the theorem for programs in normal form, and then lift it to recursion-free programs by using the preservation of the semantics of HFL**Z** formulas by reductions, and further to arbitrary programs by using the (co-)continuity of the functions represented by fixpoint-free HFL**Z** formulas. See [23] for a concrete proof.

### **7 Linear-Time Temporal Properties**

This section considers the following problem: "Given a program P and an ωregular word language L, does **InfTraces**(P)∩L = ∅ hold?". From the viewpoint of program verification, L represents the set of "bad" behaviors. This can be considered an extension of the problems considered in the previous sections.

The reduction to HFL model checking is more involved than those in the previous sections. To see the difficulty, consider the program P0:

$$(\{f = \text{if } c \text{ then } (\text{event } \mathbf{a}; f) \text{ else } (\text{event } \mathbf{b}; f)\}, \quad f),$$

where c is some boolean expression. Let L be the complement of (a∗b)ω, i.e., the set of infinite sequences that contain only finitely many b's. Following Sect. 6 (and noting that **InfTraces**(P)∩L = ∅ is equivalent to **InfTraces**(P) ⊆ (a∗b)ω in this case), one may be tempted to prepare an LTS like the one in Fig. 4 (which corresponds to the transition function of a (parity) word automaton accepting (a∗b)ω), and translate the program to an HES ΦP0 of the form:

$$(f =\_{\alpha} (c \Rightarrow \langle \mathbf{a} \rangle f) \land (\neg c \Rightarrow \langle \mathbf{b} \rangle f), \quad f),$$

where α is μ or ν. However, such a translation would not work. If c = **true**, then **InfTraces**(P0) = aω, hence **InfTraces**(P0) ∩ L = ∅; thus, α should be μ for ΦP0 to be unsatisfied. If c = **false**, however, **InfTraces**(P0) = bω, hence **InfTraces**(P0) ∩ L = ∅; thus, α must be ν for ΦP0 to be satisfied.

**Fig. 4.** LTS for (a∗b) ω

The example above suggests that we actually need to distinguish between the two occurrences of f in the body of f's definition. Note that in the then- and else-clauses respectively, f is called after different events a and b. This difference is important, since we are interested in whether b occurs infinitely often. We thus duplicate f, and replace the program with the following program P*dup*:

> ({fb = **if** c **then** (**event** a; fa) **else** (**event** b; fb), fa = **if** c **then** (**event** a; fa) **else** (**event** b; fb)}, fb).

For checking **InfTraces**(P0) ∩ L = ∅, it is now sufficient to check that fb is recursively called infinitely often. We can thus obtain the following HES:

$$((f\_b =\_\nu (c \Rightarrow \langle \mathbf{a} \rangle f\_a) \land (\neg c \Rightarrow \langle \mathbf{b} \rangle f\_b); \quad f\_a =\_\mu (c \Rightarrow \langle \mathbf{a} \rangle f\_a) \land (\neg c \Rightarrow \langle \mathbf{b} \rangle f\_b)), f\_b).$$

Note that fb and fa are bound by ν and μ respectively, reflecting the fact that b should occur infinitely often, but a need not. If c = **true**, the formula is equivalent to νfb.aμfa.afa, which is false. If c = **false**, then the formula is equivalent to νfb.bfb, which is satisfied by by the LTS in Fig. 4.

The general translation is more involved due to the presence of higher-order functions, but, as in the example above, the overall translation consists of two steps. We first replicate functions according to what events may occur between two recursive calls, and reduce the problem **InfTraces**(P) ∩L ? = ∅ to a problem of analyzing which functions are recursively called infinitely often, which we call a *call-sequence analysis*. We can then reduce the call-sequence analysis to HFL model checking in a rather straightforward manner (though the proof of the correctness is non-trivial). The resulting HFL formula actually does not contain modal operators.7 So, as in Sect. 5, the resulting problem is the validity checking of HFL formulas without modal operators.

In the rest of this section, we first introduce the call-sequence analysis problem and its reduction to HFL model checking in Sect. 7.1. We then show how to reduce the temporal verification problem **InfTraces**(P) ∩ L ? = ∅ to an instance of the call-sequence analysis problem in Sect. 7.2.

### **7.1 Call-Sequence Analysis**

We define the call-sequence analysis and reduce it to an HFL model-checking problem. As mentioned above, in the call-sequence analysis, we are interested in analyzing which functions are *recursively called* infinitely often. Here, we say that g is *recursively called from* f, if f s- −→D [s/ x--D g t, where f x-

]tf −→∗ = tf ∈ D and g "originates from" tf (a more formal definition will be given in Definition 6 below). For example, consider the following program P*app*, which is a twisted version of P*dup* above.

({app h x = h x, fb x = **if** x > 0 **then** (**event** a; app fa (x − 1)) **else** (**event** b; app fb 5), fa x = **if** x > 0 **then** (**event** a; app fa (x − 1)) **else** (**event** b; app fb 5)}, fb 5).

7 In the example above, we can actually remove a and b, as information about events has been taken into account when f was duplicated.

Then fa is "recursively called" from fb in fb 5 a −→∗ D app fa 4 −→∗ D fa 4 (and so is app). We are interested in infinite chains of recursive calls f0f1f2 ···, and which functions may occur infinitely often in each chain. For instance, the program above has the unique infinite chain (fbf 5 a )ω, in which both fa and fb occur infinitely often. (Besides the infinite chain, the program has finite chains like fb app; note that the chain cannot be extended further, as the body of app does not have any occurrence of recursive functions: app, fa and fb.) **Definition 6 (Recursive call relation, call sequences).** *Let* P = (D, f1 s-

We define the notion of "recursive calls" and call-sequences formally below.

) *be a program, with* D = {fi x˜i = ui}1≤i≤n*. We define* D := D∪{f i x˜ = ui}1≤i≤n *where* f 1,...,f n *are fresh symbols. (Thus,* D *has two copies of each function symbol, one of which is marked by .) For the terms* ti *and* tj *that do not contain marked symbols, we write* fi tiDfj tj *if (i)* [ti/xi][f 1/f1,...,f n/fn]ui - −→∗ D f j t j *and (ii)* tj *is obtained by erasing all the marks in* t j *. We write* **Callseq**(P) *for the set of (possibly infinite) sequences of function symbols:* {f1 g1 g2 ···| f1 s-Dg1 t1Dg2 -

$$\{f\_1 \, g\_1 \, g\_2 \cdots \mid f\_1 \, \widetilde{s} \leadsto\_D g\_1 \, \widetilde{t}\_1 \leadsto\_D g\_2 \, \widetilde{t}\_2 \leadsto\_D \dotsb \}.$$

*We write* **InfCallseq**(P) *for the subset of* **Callseq**(P) *consisting of infinite sequences, i.e.,* **Callseq**(P) ∩ {f1,...,fn}ω*.*

For example, for P*app* above, **Callseq**(P) is the prefix closure of {(fbf 5 a )ω} ∪ {s · app | s is a non-empty finite prefix of (fbf 5 a )ω}, and **InfCallseq**(P) is the singleton set {(fbf 5 a )ω}.

**Definition 7 (Call-sequence analysis).** *A* priority assignment *for a program* P *is a function* Ω : **funs**(P) → N *from the set of function symbols of* P *to the set* N *of natural numbers. We write* |=*csa* (P, Ω) *if every infinite callsequence* g0g1g2 ···∈ **InfCallseq**(P) *satisfies the parity condition w.r.t.* Ω*, i.e., the largest number occurring infinitely often in* Ω(g0)Ω(g1)Ω(g2)... *is even.* Call-sequence analysis *is the problem of, given a program* P *with a priority assignment* Ω*, deciding whether* |=*csa* (P, Ω) *holds.*

For example, for P*app* and the priority assignment Ω*app* = {app → 3, fa → 1, fb → 2}, |=*csa* (P*app*, Ω*app*) holds.

The call-sequence analysis can naturally be reduced to HFL model checking against the trivial LTS L0 = ({s }, ∅, ∅, s ) (or validity checking).

**Definition 8.** *Let* P = (D, t) *be a program and* Ω *be a priority assignment for* P*. The HES* Φ(P,Ω),*csa is* (D†*csa* , t†*csa* )*, where* D†*csa and* t †*csa are defined by:* {f1 x-1 = t1,...,fn x-†*csa* = f1 x-†*csa* ; ··· ; fn xn =αn tn†*csa*

n = tn} 1 =α1 t1 ( )†*csa* = **true** x†*csa* = x n†*csa* = n (t1 op t2) †*csa* = t1 †*csa* op t2 †*csa* (**if** p(t 1,...,t k) **then** t1 **else** t2) †*csa* = (p(t 1 †*csa* ,...,t k †*csa* ) ⇒ t1 †*csa* ) ∧ (¬p(t 1 †*csa* ,...,t k †*csa* ) ⇒ t2 †*csa* ) (**event** a;t) †*csa* = t †*csa* (t1 t2) †*csa* = t1 †*csa* t2 †*csa* (t1t2) †*csa* = t1 †*csa* ∧ t2 †*csa* . *Here, we assume that* Ω(fi) ≥ Ω(fi+1) *for each* i ∈ {1,...,n − 1}*, and* αi = ν *if* Ω(fi) *is even and* μ *otherwise.*

The following theorem states the soundness and completeness of the reduction. See [23] for a proof.

**Theorem 4.** *Let* P *be a program and* Ω *be a priority assignment for* P*. Then* |=*csa* (P, Ω) *if and only if* L0 |= Φ(P,Ω),*csa .*

*Example 9.* For P*app* and Ω*app* above, (P*app*, Ω*app*) †*csa* = (E, fb 5), where: E is:

app h x =μ h x; fb x =ν (x > 0 ⇒ app fa (x − 1)) ∧ (x ≤ 0 ⇒ app fb 5); fa x =μ (x > 0 ⇒ app fa (x − 1)) ∧ (x ≤ 0 ⇒ app fb 5).

Note that L0 |= (P*app*, Ω*app*) †*csa* holds.

#### **7.2 From Temporal Verification to Call-Sequence Analysis**

This subsection shows a reduction from the temporal verification problem **InfTraces**(P) ∩ L ? = ∅ to a call-sequence analysis problem ? |=*csa* (P , Ω).

For the sake of simplicity, we assume without loss of generality that every program P = (D, t) in this section is non-terminating and every infinite reduction sequence produces infinite events, so that **FullTraces**(P) = **InfTraces**(P) holds. We also assume that the ω-regular language L for the temporal verification problem is specified by using a non-deterministic, parity word automaton [10]. We recall the definition of non-deterministic, parity word automata below.

 A* run *of* A *on an* ω*-word* a0a1 ···∈ Σω *is an infinite sequence of states* ρ = ρ(0)ρ(1)··· ∈ Qω *such that (i)* ρ(0) = qI *, and (ii)* ρ(i + 1) ∈ δ(ρ(i), ai) *for each* i ∈ ω*. An* ω*-word* w ∈ Σω *is* accepted *by* A *if, there exists a run* ρ *of* A *on* w *such that* **max**{Ω(q) | q ∈ **Inf**(ρ)} *is even, where* **Inf**(ρ) *is the set of states that occur infinitely often in* ρ*. We write* L(A) *for the set of* ω*-words accepted by* A*.*

For technical convenience, we assume below that δ(q, a) = ∅ for every q ∈ Q and a ∈ Σ; this does not lose generality since if δ(q, a) = ∅, we can introduce a new "dead" state q*dead* (with priority 1) and change δ(q, a) to {q*dead* }. Given a parity automaton A, we refer to each component of A by QA, ΣA, δA, qI,A and ΩA.

*Example 10.* Consider the automaton Aab = ({qa, qb}, {a, b}, δ, qa, Ω), where δ is as given in Fig. 4, Ω(qa) = 0, and Ω(qb) = 1. Then, L(Aab) = (a∗b)ω = (a∗b)∗aω. The goal of this subsection is, given a program P and a parity word automaton A, to construct another program P and a priority assignment Ω for P , such that **InfTraces**(P) ∩ L(A) = ∅ if and only if |=*csa* (P , Ω).

Note that a necessary and sufficient condition for **InfTraces**(P) ∩ L(A) = ∅ is that no trace in **InfTraces**(P) has a run whose priority sequence satisfies the parity condition; in other words, for every sequence in **InfTraces**(P), and for every run for the sequence, the largest priority that occurs in the associated priority sequence is odd. As explained at the beginning of this section, we reduce this condition to a call sequence analysis problem by appropriately duplicating functions in a given program. For example, recall the program P0:

$$(\{f = \text{if } c \text{ then } (\text{event } \mathbf{a}; f) \text{ else } (\text{event } \mathbf{b}; f)\}, f) \dots$$

It is translated to P 0:

$$\begin{array}{l} ({\{f\_b = \text{if } c \text{ then } (\text{event } a; f\_a) \text{ else } (\text{event } b; f\_b)},\\ {f\_a = \text{if } c \text{ then } (\text{event } a; f\_a) \text{ else } (\text{event } b; f\_b)}, \end{array}$$

where c is some (closed) boolean expression. Since the largest priorities encountered before calling fa and fb (since the last recursive call) respectively are 0 and 1, we assign those priorities plus 1 (to flip odd/even-ness) to fa and fb respectively. Then, the problem of **InfTraces**(P0) ∩ L(A) = ∅ is reduced to |=*csa* (P 0, {fa → 1, fb → 2}). Note here that the priorities of fa and fb represent *summaries* of the priorities (plus one) that occur in the run of the automaton until fa and fb are respectively called since the last recursive call; thus, the largest priority of states that occur infinitely often in the run for an infinite trace is equivalent to the largest priority that occurs infinitely often in the sequence of summaries (Ω(f1)−1)(Ω(f2)−1)(Ω(f3)−1)··· computed from a corresponding call sequence f1f2f3 ···.

Due to the presence of higher-order functions, the general reduction is more complicated than the example above. First, we need to replicate not only function symbols, but also arguments. For example, consider the following variation P1 of P0 above:

$$(\{g \: k = \text{if } c \text{ then } (\text{event } \mathbf{a}; k) \text{ else } (\text{event } \mathbf{b}; k), \quad f = g \, f\}, \quad f \text{)}.$$

Here, we have just made the calls to f indirect, by preparing the function g. Obviously, the two calls to k in the body of g must be distinguished from each other, since different priorities are encountered before the calls. Thus, we duplicate the argument k, and obtain the following program P 1:

$$(\{g \: k\_a \: k\_b = \text{if } c \text{ then } (\text{event } a; k\_a) \text{ else } (\text{event } b; k\_b), f\_a = g \; f\_a \; f\_b, f\_b = g \; f\_a \; f\_b\}, f\_a).$$

Then, for the priority assignment Ω = {fa → 1, fb → 2, g → 1}, **InfTraces**(P1)∩ L(Aab) = ∅ if and only if |=*csa* (P 1, Ω). Secondly, we need to take into account not only the priorities of states visited by A, but also the states themselves. For example, if we have a function definition f h = h(**event** a; f h), the largest priority encountered before f is recursively called in the body of f depends on the priorities encountered inside h, *and also* the state of A when h uses the argument **event** a; f (because the state after the a event depends on the previous state in general). We, therefore, use *intersection types* (a la Kobayashi and Ong's intersection types for HORS model checking [21]) to represent summary information on how each function traverses states of the automaton, and replicate each function and its arguments for each type. We thus formalize the translation as an intersection-type-based program transformation; related transformation techniques are found in [8,11,12,20,38].

**Definition 10.** *Let* A = (Q, Σ, δ, qI , Ω) *be a non-deterministic parity word automaton. Let* q *and* m *range over* Q *and the set codom*(Ω) *of priorities respectively. The set* **Types**A *of* intersection types*, ranged over by* θ*, is defined by:*

$$\theta \colon= q \mid \rho \to \theta \qquad\qquad \rho \colon= \mathsf{int} \mid \bigwedge\_{1 \le i \le k} (\theta\_i, m\_i)$$

*We assume a certain total order* < *on* **Types**A × N*, and require that in* 1≤i≤k(θi, mi)*,* (θi, mi) < (θj , mj ) *holds for each* i<j*.* We often write (θ1, m1) ∧···∧ (θk, mk) for

1≤i≤k(θi, mi), and when k = 0. Intuitively, the type q describes expressions of simple type , which may be evaluated when the automaton A is in the state q (here, we have in mind an execution of the *product* of a program and the automaton, where the latter takes events produced by the program and changes its states). The type ( 1≤i≤k(θi, mi)) → θ describes functions that take an argument, use it according to types θ1,...,θk, and return a value of type θ. Furthermore, the part mi describes that the argument may be used as a value of type θi only when the largest priority visited since the function is called is mi. For example, given the automaton in Example 10, the function λx.(**event** a; x) may have types (qa, 0) → qa and (qa, 0) → qb, because the body may be executed from state qa or qb (thus, the return type may be any of them), but x is used only when the automaton is in state qa and the largest priority visited is 1. In contrast, λx.(**event** b; x) have types (qb, 1) → qa and (qb, 1) → qb.

Using the intersection types above, we shall define a type-based transformation relation of the form Γ A t : θ ⇒ t , where t and t are the source and target terms of the transformation, and Γ, called an *intersection type environment*, is a finite set of type bindings of the form x : int or x : (θ, m, m ). We allow multiple type bindings for a variable x except for x:int (i.e. if x:int ∈ Γ, then this must be the unique type binding for x in Γ). The binding x : (θ, m, m ) means that x should be used as a value of type θ when the largest priority visited is m; m is auxiliary information used to record the largest priority encountered so far.

The transformation relation Γ A t : θ ⇒ t is inductively defined by the rules in Fig. 5. (For technical convenience, we have extended terms with λ-abstractions; they may occur only at top-level function definitions.) In the figure, [k] denotes the set {i ∈ N | 1 ≤ i ≤ k}. The operation Γ ↑ m used in the figure is defined by:

$$\Gamma \upharpoonright m = \{x : \mathbf{int} \mid x : \mathbf{int} \in \Gamma\} \cup \{x : (\theta, m\_1, \mathbf{max}(m\_2, m)) \mid x : (\theta, m\_1, m\_2) \in \Gamma\}$$

The operation is applied when the priority m is encountered, in which case the largest priority encountered is updated accordingly. The key rules are IT-Var, IT-Event, IT-App, and IT-Abs. In IT-Var, the variable x is replicated for each type; in the target of the translation, xθ,m and xθ-,m are treated as different variables if (θ,m) = (θ , m ). The rule IT-Event reflects the state change caused by the event a to the type and the type environment. Since the state change may be non-deterministic, we transform t for each of the next states q1,...,qn, and combine the resulting terms with non-deterministic choice. The rule IT-App and IT-Abs replicates function arguments for each type. In addition, in IT-App, the operation Γ ↑ mi reflects the fact that t2 is used as a value of type θi after the priority mi is encountered. The other rules just transform terms in a compositional manner. If target terms are ignored, the entire rules are close to those of Kobayashi and Ong's type system for HORS model checking [21].

**Fig. 5.** Type-based transformation rules for terms

We now define the transformation for programs. A *top-level type environment* Ξ is a finite set of type bindings of the form x : (θ,m). Like intersection type environments, Ξ may have more than one binding for each variable. We write Ξ A t : θ to mean {x : (θ, m, 0) | x : (θ,m) ∈ Ξ} A t : θ. For a set D of function definitions, we write Ξ A D ⇒ D if *dom*(D ) = { fθ,m | f : (θ,m) ∈ Ξ } and Ξ A D(f) : θ ⇒ D (fθ,m) for every f :(θ,m) ∈ Ξ. For a program P = (D, t), we write Ξ A P ⇒ (P , Ω ) if P = (D , t ), Ξ A D ⇒ D and Ξ A t : qI ⇒ t , with Ω (fθ,m) = m+ 1 for each fθ,m ∈ *dom*(D ). We just write A P ⇒ (P , Ω ) if Ξ A P ⇒ (P , Ω ) holds for some Ξ.

*Example 11.* Consider the automaton Aab in Example 10, and the program P2 = (D2, f 5) where D2 consists of the following function definitions:

> g k = (**event** a; k)-(**event** b; k), f x = **if** x > 0 **then** g (f(x − 1)) **else** (**event** b; f 5).

Let Ξ be: {g : ((qa, 0) ∧ (qb, 1) → qa, 0), g : ((qa, 0) ∧ (qb, 1) → qb, 0), f : (int → qa, 0), f : (int → qb, 1)}. Then, Ξ A P1 ⇒ ((D 2, fint→qa,0 5), Ω) where:

$$\begin{array}{llll} D\_{2}^{\prime} = \{ g\_{(q\_{a},0) \wedge (q\_{b},1) \rightarrow q\_{a},0} \, k\_{q\_{a},0} \, k\_{q\_{b},1} = t\_{g}, & g\_{(q\_{a},0) \wedge (q\_{b},1) \rightarrow q\_{b},0} \, k\_{q\_{a},0} \, k\_{q\_{b},1} = t\_{g}, \\\ f\_{\texttt{int-eq},q\_{a}} \, 0 \, x\_{\texttt{int}} = t\_{f,q\_{a}}, & f\_{\texttt{int-eq},q\_{1}} \, x\_{\texttt{int}} = t\_{f,q\_{b}} \} \\\ t\_{g} = (\textbf{event} \, \texttt{a}; k\_{q\_{a},0}) \square(\textbf{event} \, \texttt{b}; k\_{q\_{b},1}), \\\ t\_{f,q} = \textbf{if} \, x\_{\texttt{int}} > 0 \, \textbf{then} \\\ f\_{(q\_{a},0) \wedge (q\_{b},1) \rightarrow q,0} \, (f\_{\texttt{int-eq},q\_{a}} \, (x\_{\texttt{int}} - 1)) \, (f\_{\texttt{int-eq},q\_{b}} \, 1 \, (x\_{\texttt{int}} - 1)) \\\ \textbf{else} \, (\textbf{event} \, \texttt{b}; f\_{\texttt{int-eq},b\_{1}} \, 5), & \text{(for each } q \in \{q\_{a}, q\_{b}\}) \\\ \Omega = \{g\_{(q\_{a},0) \wedge (q\_{b},1) \rightarrow q\_{a},0} \, \forall 1, g\_{(q\_{a},0) \wedge (q\_{b},1) \rightarrow q\_{b},0} \, \forall 1, f\_{\texttt{int-eq} \, \texttt{b}\_{b},1 \rightarrow q\_{b},1} \, \mathtt{2} \}. \end{array}$$

Notice that f, g, and the arguments of g have been duplicated. Furthermore, whenever fθ,m is called, the largest priority that has been encountered since the last recursive call is m. For example, in the then-clause of fint→qa,0, fint→qb,1(x−1) may be called through g(qa,0)∧(qb,1)→qa,0. Since g(qa,0)∧(qb,1)→qa,0 uses the second argument only after an event b, the largest priority encountered is 1. This property is important for the correctness of our reduction.

The following theorems below claim that our reduction is sound and complete, and that there is an effective algorithm for the reduction: see [23] for proofs.

**Theorem 5.** *Let* P *be a program and* A *be a parity automaton. Suppose that* Ξ A P ⇒ (P , Ω)*. Then* **InfTraces**(P)∩ L(A) = ∅ *if and only if* |=*csa* (P , Ω)*.*

**Theorem 6.** *For every* P *and* A*, one can effectively construct* Ξ*,* P *and* Ω *such that* Ξ A P ⇒ (P , Ω)*.*

The proof of Theorem 6 above also implies that the reduction from temporal property verification to call-sequence analysis can be performed in polynomial time. Combined with the reduction from call-sequence analysis to HFL model checking, we have thus obtained a polynomial-time reduction from the temporal verification problem **InfTraces**(P) ? ⊆ L(A) to HFL model checking.

### **8 Related Work**

As mentioned in Sect. 1, our reduction from program verification problems to HFL model checking problems has been partially inspired by the translation of Kobayashi et al. [19] from HORS model checking to HFL model checking. As in their translation (and unlike in previous applications of HFL model checking [28, 42]), our translation switches the roles of properties and models (or programs) to be verified. Although a combination of their translation with Kobayashi's reduction from program verification to HORS model checking [17,18] yields an (indirect) translation from *finite-data* programs to pure HFL model checking problems, the combination does not work for infinite-data programs. In contrast, our translation is sound and complete even for infinite-data programs. Among the translations in Sects. 5, 6 and 7, the translation in Sect. 7.2 shares some similarity to their translation, in that functions and their arguments are replicated for each priority. The actual translations are however quite different; ours is typedirected and optimized for a given automaton, whereas their translation is not. This difference comes from the difference of the goals: the goal of [19] was to clarify the relationship between HORS and HFL, hence their translation was designed to be independent of an automaton. The proof of the correctness of our translation in Sect. 7 is much more involved due to the need for dealing with integers. Whilst the proof of [19] could reuse the type-based characterization of HORS model checking [21], we had to generalize arguments in both [19,21] to work on infinite-data programs.

Lange et al. [28] have shown that various process equivalence checking problems (such as bisimulation and trace equivalence) can be reduced to (pure) HFL model checking problems. The idea of their reduction is quite different from ours. They reduce processes to LTSs, whereas we reduce programs to HFL formulas.

Major approaches to automated or semi-automated higher-order program verification have been HORS model checking [17,18,22,27,31,33,43], (refinement) type systems [14,24,34–36,39,41,44], Horn clause solving [2,7], and their combinations. As already discussed in Sect. 1, compared with the HORS model checking approach, our new approach provides more uniform, streamlined methods. Whilst the HORS model checking approach is for fully automated verification, our approach enables various degrees of automation: after verification problems are automatically translated to HFL**Z** formulas, one can prove them (i) interactively using a proof assistant like Coq (see [23]), (ii) semi-automatically, by letting users provide hints for induction/co-induction and discharging the rest of proof obligations by (some extension of) an SMT solver, or (iii) fully automatically by recasting the techniques used in the HORS-based approach; for example, to deal with the ν-only fragment of HFL**Z**, we can reuse the technique of predicate abstraction [22]. For a more technical comparison between the HORS-based approach and our HFL-based approach, see [23].

As for type-based approaches [14,24,34–36,39,41,44], most of the refinement type systems are (i) restricted to safety properties, and/or (ii) incomplete. A notable exception is the recent work of Unno et al. [40], which provides a relatively complete type system for the classes of properties discussed in Sect. 5. Our approach deals with a wider class of properties (cf. Sects. 6 and 7). Their "relative completeness" property relies on Godel coding of functions, which cannot be exploited in practice.

The reductions from program verification to Horn clause solving have recently been advocated [2–4] or used [34,39] (via refinement type inference problems) by a number of researchers. Since Horn clauses can be expressed in a fragment of HFL without modal operators, fixpoint alternations (between ν and μ), and higher-order predicates, our reductions to HFL model checking may be viewed as extensions of those approaches. Higher-order predicates and fixpoints over them allowed us to provide sound and complete characterizations of properties of higher-order programs for a wider class of properties. Bjørner et al. [4] proposed an alternative approach to obtaining a complete characterization of safety properties, which defunctionalizes higher-order programs by using algebraic data types and then reduces the problems to (first-order) Horn clauses. A disadvantage of that approach is that control flow information of higher-order programs is also encoded into algebraic data types; hence even for finite-data higher-order programs, the Horn clauses obtained by the reduction belong to an undecidable fragment. In contrast, our reductions yield pure HFL model checking problems for finite-data programs. Burn et al. [7] have recently advocated the use of *higherorder* (constrained) Horn clauses for verification of safety properties (i.e., which correspond to the negation of may-reachability properties discussed in Sect. 5.1 of the present paper) of higher-order programs. They interpret recursion using the least fixpoint semantics, so their higher-order Horn clauses roughly corresponds to a fragment of the HFL**Z** without modal operators and fixpoint alternations. They have not shown a general, concrete reduction from safety property verification to higher-order Horn clause solving.

The characterization of the reachability problems in Sect. 5 in terms of formulas without modal operators is a reminiscent of predicate transformers [9,13] used for computing the weakest preconditions of imperative programs. In particular, [5] and [13] respectively used least fixpoints to express weakest preconditions for while-loops and recursions.

### **9 Conclusion**

We have shown that various verification problems for higher-order functional programs can be naturally reduced to (extended) HFL model checking problems. In all the reductions, a program is mapped to an HFL formula expressing the property that the behavior of the program is correct. For developing verification tools for higher-order functional programs, our reductions allow us to focus on the development of (automated or semi-automated) HFL**Z** model checking tools (or, even more simply, theorem provers for HFL**Z** without modal operators, as the reductions of Sects. 5 and 7 yield HFL formulas without modal operators). To this end, we have developed a prototype model checker for pure HFL (without integers), which will be reported in a separate paper. Work is under way to develop HFL**Z** model checkers by recasting the techniques [22,26,27,43] developed for the HORS-based approach, which, together with the reductions presented in this paper, would yield fully automated verification tools. We have also started building a Coq library for interactively proving HFL**Z** formulas, as briefly discussed in [23]. As a final remark, although one may fear that our reductions may map program verification problems to "harder" problems due to the expressive power of HFL**Z**, it is actually not the case at least for the classes of problems in Sects. 5 and 6, which use the only alternation-free fragment of HFL**Z**. The model checking problems for μ-only or ν-only HFL**Z** are semi-decidable and co-semi-decidable respectively, like the source verification problems of may/must-reachability and their negations of closed programs.

**Acknowledgment.** We would like to thank anonymous referees for useful comments. This work was supported by JSPS KAKENHI Grant Number JP15H05706 and JP16K16004.

### **References**

**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.

### **Quantitative Analysis of Smart Contracts**

Krishnendu Chatterjee1, Amir Kafshdar Goharshady1(B), and Yaron Velner2

1 IST Austria (Institute of Science and Technology Austria), Klosterneuburg, Austria

<EMAIL_ADDRESS>2 Hebrew University of Jerusalem, Jerusalem, Israel

<EMAIL_ADDRESS>
**Abstract.** Smart contracts are computer programs that are executed by a network of mutually distrusting agents, without the need of an external trusted authority. Smart contracts handle and transfer assets of considerable value (in the form of crypto-currency like Bitcoin). Hence, it is crucial that their implementation is bug-free. We identify the utility (or expected payoff) of interacting with such smart contracts as the basic and canonical quantitative property for such contracts. We present a framework for such quantitative analysis of smart contracts. Such a formal framework poses new and novel research challenges in programming languages, as it requires modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior and modeling utilities which are not specified as standard temporal properties such as safety and termination. While game-theoretic incentives have been analyzed in the security community, their analysis has been restricted to the very special case of stateless games. However, to analyze smart contracts, stateful analysis is required as it must account for the different program states of the protocol. Our main contributions are as follows: we present (i) a simplified programming language for smart contracts; (ii) an automatic translation of the programs to state-based games; (iii) an abstractionrefinement approach to solve such games; and (iv) experimental results on real-world-inspired smart contracts.

### **1 Introduction**

In this work we present a quantitative stateful game-theoretic framework for formal analysis of smart-contracts.

*Smart Contracts.* Hundreds of crypto-currencies are in use today, and investments in them are increasing steadily [24]. These currencies are not controlled by any central authority like governments or banks, instead they are governed by the *blockchain* protocol, which dictates the rules and determines the outcomes, e.g., the validity of money transactions and account balances. Blockchain was initially used for peer-to-peer Bitcoin payments [43], but recently it is also used for running programs (called smart contracts). A *smart contract* is a program that runs on the blockchain, which enforces its correct execution (i.e., that

A longer version of this article is available in [19].

c The Author(s) 2018

A. Ahmed (Ed.): ESOP 2018, LNCS 10801, pp. 739–767, 2018. https://doi.org/10.1007/978-3-319-89884-1\_26

it is running as originally programmed). This is done by encoding semantics in crypto-currency transactions. For example, Bitcoin transaction scripts allow users to specify conditions, or contracts, which the transactions must satisfy prior to acceptance. Transaction scripts can encode many useful functions, such as validating that a payer owns a coin she is spending or enforcing rules for multi-party transactions. The Ethereum crypto-currency [16] allows arbitrary stateful Turing-complete conditions over the transactions which gives rise to smart contracts that can implement a wide range of applications, such as financial instruments (e.g., financial derivatives or wills) or autonomous governance applications (e.g., voting systems). The protocols are globally specified and their implementation is decentralized. Therefore, there is no central authority and they are immutable. Hence, the economic consequences of bugs in a smart contract cannot be reverted.

*Types of Bugs.* There are two types of bugs with monetary consequences:

*DAO Attack: Interaction of Two Types of Bugs.* Quite interestingly a coding bug can incentivize dishonest behavior as in the famous DAO attack [48]. The Decentralized Autonomous Organization (DAO) [38] is an Ethereum smart contract [51]. The contract consists of investor-directed venture capital fund. On June 17, 2016 an attacker exploited a bug in the contract to extract \$80 million [48]. Intuitively, the root cause was that the contract allowed users to first get hold of their funds, and only then updated their balance records while a semantic detail allowed the attacker to withdraw multiple times before the update.

*Necessity of Formal Framework.* Since bugs in smart contracts have direct economic consequences and are irreversible, they have the same status as safetycritical errors for programs and reactive systems and must be detected before deployment. Moreover, smart contracts are deployed rapidly. There are over a million smart contracts in Ethereum, holding over 15 billion dollars at the time of writing [31]. It is impossible for security researchers to analyze all of them, and lack of automated tools for programmers makes them error prone. Hence, a formal analysis framework for smart contract bugs is of great importance.

*Utility Analysis.* In verification of programs, specifying objectives is non-trivial and a key goal is to consider specification-less verification, where basic properties are considered canonical. For example, termination is a basic property in program analysis; and data-race freedom or serializability are basic properties in concurrency. Given these properties, models are verified wrt them without considering any other specification. For smart contracts, describing the correct specification that prevents dishonest behavior is more challenging due to the presence of game-like interactions. We propose to consider the expected user utility (or payoff) that is guaranteed even in presence of adversarial behavior of other agents as a canonical property. Considering malicious adversaries is standard in game theory. For example, the expected utility of a fair lottery is 0. An analysis reporting a different utility signifies a bug.

*New Research Challenges.* Coding bugs are detected by classic verification, program analysis, and model checking tools [23,39]. However, a formal framework for incentivization bugs presents a new research challenge for the programming language community. Their analysis must overcome two obstacles: (a) the framework will have to handle game-theoretic aspects to model interactions and incentives for dishonest behavior; and (b) it will have to handle properties that cannot be deduced from standard temporal properties such as safety or termination, but require analysis of monetary gains (i.e., quantitative properties).

While game-theoretic incentives are widely analyzed by the security community (e.g., see [13]), their analysis is typically restricted to the very special case of one-shot games that do not consider different states of the program, and thus the consequences of decisions on the next state of the program are ignored. In addition their analysis is typically ad-hoc and stems from brainstorming and special techniques. This could work when very few protocols existed (e.g., when bitcoin first emerged) and deep thought was put into making them elegant and analyzable. However, the fast deployment of smart contracts makes it crucial to automate the process and make it accessible to programmers.

*Our Contribution.* In this work we present a formal framework for quantitative analysis of utilities in smart contracts. Our contributions are as follows:

(namely, turn-based games) have been studied in verification and reactive synthesis, there are no practical methods to solve general concurrent quantitative games. To the best of our knowledge, there are no tools to solve quantitative concurrent games other than academic examples of few states, and we present the first practical method to solve quantitative concurrent games that scales to real-world smart contract analysis.

In summary, our contributions range from (i) modeling of smart contracts as state-based games, to (ii) an abstraction-refinement approach to solve such games, to (iii) experimental results on real-world smart contracts.

### **2 Background on Ethereum Smart Contracts**

### **2.1 Programmable Smart Contracts**

Ethereum [16] is a decentralized virtual machine, which runs programs called contracts. Contracts are written in a Turing-complete bytecode language, called Ethereum Virtual Machine (EVM) bytecode [53]. A contract is invoked by calling one of its functions, where each function is defined by a sequence of instructions. The contract maintains a persistent internal state and can receive (transfer) currency from (to) users and other contracts. Users send transactions to the Ethereum network to invoke functions. Each transaction may contain input parameters for the contract and an associated monetary amount, possibly 0, which is transferred from the user to the contract.

Upon receiving a transaction, the contract collects the money sent to it, executes a function according to input parameters, and updates its internal state. All transactions are recorded on a decentralized ledger, called blockchain. A sequence of transactions that begins from the creation of the network uniquely determines the state of each contract and balances of users and contracts. The blockchain does not rely on a trusted central authority, rather, each transaction is processed by a large network of mutually untrusted peers called miners. Users constantly broadcast transactions to the network. Miners add transactions to the blockchain via a proof-of-work consensus protocol [43].

*Subtleties.* In this work, for simplicity, we ignore some details in the underlying protocol of Ethereum smart contract. We briefly describe these details below:

– *Transaction fees.* In exchange for including her transactions in the blockchain, a user pays transaction fees to the miners, proportionally to the execution time of her transaction. This fact could slightly affect the monetary analysis of the user gain, but could also introduce bugs in a program, as there is a bound on execution time that cannot be exceeded. Hence, it is possible that some functions could never be called, or even worse, a user could actively give input parameters that would prevent other users from invoking a certain function.

### **2.2 Tokens and User Utility**

A user's utility is determined by the Ether she spends and receives, but could also be affected by the state of the contract. Most notably, smart contracts are used to issue *tokens*, which can be viewed as a stake in a company or an organization, in return to an Ether (or tokens) investment (see an example in Fig. 1). These tokens are *transferable* among users and are traded in exchanges in return to Ether, Bitcoin and Fiat money. At the time of writing, smart contracts instantiate tokens worth billions of dollars [32]. Hence, gaining or losing tokens has clear utility for the user. At a larger scope, user utility could also be affected by more abstract storage changes. Some users would be willing to pay to have a contract declare them as Kings of Ether [4], while others could gain from registering their domain name in a smart contract storage [40]. In the examples provided in this work we mainly focus on utility that arises from Ether, tokens and the like. However, our approach is general and can model any form of utility by introducing auxiliary utility variables and definitions.

**Fig. 1.** Token contract example.

### **3 Programming Language for Smart Contracts**

In this section we present our programming language for smart contracts that supports concurrent interactions between parties. A party denotes an agent that decides to interact with the contract. A contract is a tuple C = (N, I,M, R, X0, F, T) where X := N ∪ I ∪ M is a set of variables, R describes the range of values that can be stored in each variable, X0 is the initial values stored in variables, F is a list of functions and T describes for each function, the time segment in which it can be invoked. We now formalize these concepts.

*Variables.* There are three distinct and disjoint types of variables in X:

*Bounds and Initial Values.* The tuple R = (R, R) where R, R : N ∪ M → Z represent lower and upper bounds for integer values that can be stored in a variable. For example, if n ∈ N, then n can only store integers between R(n) and R(n). Similarly, if m ∈ M is a mapping and i ∈ I stores an address to a party in the contract, then m [i] can save integers between R(m) and R(m). The function X0 : X → Z ∪ {Null} assigns an initial value to every variable. The assigned value is an integer in case of numeric and mapping variables, i.e., a mapping variable maps everything to its initial value by default. Id variables can either be initialized by Null or an id used by one of the parties.

*Functions and Timing.* The sequence F =< f1, f2,...,fn > is a list of functions and T = (T, T), where T, T : F → N. The function fi can only be invoked in time-frame T(fi) = - T(fi), T(fi) . The contract uses a global clock, for example the current block number in the blockchain, to keep track of time.

Note that we consider a single contract, and interaction between multiple contracts is a subject of future work.

### **3.1 Syntax**

We provide a simple overview of our contract programming language. Our language is syntactically similar to Solidity [30], which is a widely used language for writing Ethereum contracts. A translation mechanism for different aspects is discussed in [19]. An example contract, modeling a game of rock-paper-scissors, is given in Fig. 2. Here, a party, called issuer has issued the contract and taken the role of Alice. Any other party can join the contract by registering as Bob and then playing rock-paper-scissors. To demonstrate our language, we use a bidding mechanism.

*Declaration of Variables.* The program begins by declaring variables1, their type, name, range and initial value. For example, Bids is a map variable that assigns a value between 0 and 100 to every id. This value is initially 0. Line numbers (labels) are defined in Sect. 3.2 below and are not part of the syntax.

*Declaration of Functions.* After the variables, the functions are defined one-byone. Each function begins with the keyword function followed by its name and

1 For simplicity, we demonstrate our method with global variables only. However, the method is applicable to general variables as long as their ranges are well-defined at each point of the program.

**Fig. 2.** A rock-paper-scissors contract.

the time interval in which it can be called by parties. Then comes a list of input parameters. Each parameter is of the form variable : party which means that the designated party can choose a value for that variable. The chosen value is required to be in the range specified for that variable. The keyword caller denotes the party that has invoked this function and payable signifies that the party should not only decide a value, but must also pay the amount she decides. For example, registerBob can be called in any time between 1 and 10 by any of the parties. At each such invocation the party that has called this function must pay some amount which will be saved in the variable bid. After the decisions and payments are done, the contract proceeds with executing the function.

*Types of Functions.* There are essentially two types of functions, depending on their parameters. *One-party functions*, such as registerBob and getReward require parameters from caller only, while *multi-party functions*, such as play ask several, potentially different, parties for input. In this case all parties provide their input decisions and payments concurrently and without being aware of the choices made by other parties, also a default value is specified for every decision in case a relevant party does not take part.

*Summary.* Putting everything together, in the contract specified in Fig. 2, any party can claim the role of Bob between time 1 and time 10 by paying a bid to the contract, if the role is not already occupied. Then at time 11 one of the parties calls play and both parties have until time 15 to decide which choice (rock, paper, scissors or none) they want to make. Then the winner can call getReward and collect her prize.

### **3.2 Semantics**

In this section we present the details of the semantics. In our programming language there are several key aspects which are non-standard in programming languages, such as the notion of time progress, concurrency, and interactions of several parties. Hence we present a detailed description of the semantics. We start with the requirements.

*Requirements.* In order for a contract to be considered valid, other than following the syntax rules, a few more requirements must be met, which are as follows:

*Overview of Time Progress.* Initially, the time is 0. Let Ft be the set of functions executable at time t, i.e., Ft = {fi ∈ F|t ∈ T(fi)}, then Ft is either empty or contains one or more one-party functions or consists of a single multi-party function. We consider the following cases:

The clock ticks when there are no more valid requests for setting a value for a variable or making a payment. This continues until we reach time T(fi). At this time parties can no longer change their choices and the choices become visible to everyone. The contract proceeds with execution of the function. If a party fails to make a payment/decision or if Null is asked to make a payment or a decision, default behavior will be enforced. Default value for payments is 0 and default behavior for other variables is defined as part of the syntax. For example, in function play of Fig. 2, if a party does not choose, a default value of 0 is enforced and given the rest of this function, this will lead to a definite loss.

Given the notion of time progress we proceed to formalize the notion of "runs" of the contract. This requires the notion of labels, control-flow graphs, valuations, and states, which we describe below.

*Labels.* Starting from 0, we give the contract, beginning and end points of every function, and every command a label. The labels are given in order of appearance. As an example, see the labels in parentheses in Fig. 2.

*Entry and Exit Labels.* We denote the first (beginning point) label in a function fi by i and its last (end point) label by i.

*Control Flow Graphs (CFGs).* We define the control flow graph CFGi of the function fi in the standard manner, i.e. CFGi = (V,E), where there is a vertex corresponding to every labeled entity inside fi. Each edge e ∈ E has a condition *cond*(e) which is a boolean expression that must be true when traversing that edge. For more details see [19].

*Valuations.* A valuation is a function *val*, assigning a value to every variable. Values for numeric variables must be integers in their range, values for identity variables can be party ids or Null and a value assigned to a map variable m must be a function *val*(m) such that for each identity i, we have R(m) ≤ *val*(m)(i) ≤ R(m). Given a valuation, we extend it to expressions containing mathematical operations in the straight-forward manner.

*States.* A state of the contract is a tuple s = (t, b, l, *val*, c), where t is a time stamp, b ∈ N ∪ {0} is the current balance of the contract, i.e., the total amount of payment to the contract minus the total amount of payouts, l is a label (that is being executed), *val* assigns values to variables and c ∈ P ∪{⊥}, is the caller of the current function. c =⊥ corresponds to the case where the caller is undefined, e.g., when no function is being executed. We use S to denote the set of all states that can appear in a run of the contract as defined below.

*Runs.* A run ρ of the contract is a finite sequence {ρj = (tj , bj , lj , *val*j , cj )} r j=0 of states, starting from (0, 0, 0, X0, ⊥), that follows all rules of the contract and ends in a state with time-stamp tr > maxf*i* T(fi). These rules must be followed when switching to a new state in a run:

– The clock can only tick when there are no valid pending requests for running a one-party function or deciding or paying in multi-party functions.

*Remark 1.* Note that in our semantics each function body completes its execution in a single tick of the clock. However, ticks might contain more than one function call and execution.

*Run Prefixes.* We use H to mean the set of all prefixes of runs and denote the last state in η ∈ H by *end*(η). A run prefix η is an extension of η if it can be obtained by adding one state to the end of η.

*Probability Distributions.* Given a finite set X , a probability distribution on X is a function δ : X → [0, 1] such that x∈X δ(x) = 1. Given such a distribution, its support, Supp(δ), is the set of all x ∈ X such that δ(x) > 0. We denote the set of all probability distributions on X by Δ(X ).

Typically for programs it suffices to define runs for the semantics. However, given that there are several parties in contracts, their semantics depends on the possible choices of the parties. Hence we need to define policies for parties, and such policies will define probability distribution over runs, which constitute the semantics for contracts. To define policies we first define moves.

*Moves.* We use M for the set of all moves. The moves that can be taken by parties in a contract can be summarized as follows:

*Permitted Moves.* We define Pi : S → M, so that Pi(s) is the set of permitted moves for the party with identity i if the contract is in state s = (t, b, l, *val*, pj ). It is formally defined as follows:

*Policies and Randomized Policies.* A policy πi for party i is a function πi : H → A, such that for every η ∈ H, πi(η) ∈ Pi(*end*(η)). Intuitively, a policy is a way of deciding what move to use next, given the current run prefix. A policy profile π = (πi) is a sequence assigning one policy to each party i. The policy profile π defines a unique run ρπ of the contract which is obtained when parties choose their moves according to π. A randomized policy ξi for party i is a function ξi : H → Δ(M), such that Supp(ξi(s)) ⊆ Pi(s). A randomized policy assigns a probability distribution over all possible moves for party i given the current run prefix of the contract, then the party can follow it by choosing a move randomly according to the distribution. We use Ξ to denote the set of all randomized policy profiles, Ξi for randomized policies of i and Ξ−i to denote the set of randomized policy profiles for all parties except i. A randomized policy profile ξ is a sequence (ξi) assigning one randomized policy to each party. Each such randomized policy profile induces a unique probability measure on the set of runs, which is denoted as Probξ [·]. We denote the expectation measure associated to Probξ [·] by Eξ [·].

### **3.3 Objective Function and Values of Contracts**

As mentioned in the introduction we identify expected payoff as the canonical property for contracts. The previous section defines expectation measure given randomized policies as the basic semantics. Given the expected payoff, we define values of contracts as the worst-case guaranteed payoff for a given party. We formalize the notion of objective function (the payoff function).

*Objective Function.* An objective o for a party p is in one of the following forms:

Informally, p is trying to choose her moves so as to maximize o.

*Run Outcomes.* Given a run ρ of the program and an objective o for party p, the outcome κ(ρ, o, p) is the value of o computed using the valuation at *end*(ρ) for all variables and accounting for payments in ρ to compute p+ and p−.

*Contract Values.* Since we consider worst-case guaranteed payoff, we consider that there is an objective o for a single party p which she tries to maximize and all other parties are adversaries who aim to minimize o. Formally, given a contract C and an objective o for party p, we define the value of contract as:

$$\mathsf{V}(C, o, p) := \sup\_{\xi\_p \in \Xi\_p} \inf\_{\xi\_-, p \in \Xi\_{-p}} \mathbb{E}^{(\xi\_p, \xi\_{-p})} \left[ \kappa(\rho, o, p) \right],$$

2 We are also assuming, as in many programming languages, that True = 1 and False = 0.

This corresponds to p trying to maximize the expected value of o and all other parties maliciously colluding to minimize it. In other words, it provides the worstcase guarantee for party p, irrespective of the behavior of the other parties, which in the worst-case is adversarial to party p.

### **3.4 Examples**

One contribution of our work is to present the simplified programming language, and to show that this simple language can express several classical smart contracts. To demonstrate the applicability, we present several examples of classical smart contracts in this section. In each example, we present a contract and a "buggy" implementation of the same contract that has a different value. In Sect. 6 we show that our automated approach to analyze the contracts can compute contract values with enough precision to differentiate between the correct and the buggy implementation. All of our examples are motivated from well-known bugs that have happened in real life in Ethereum.

**Rock-Paper-Scissors.** Let our contract be the one specified in Fig. 2 and assume that we want to analyze it from the point of view of the issuer p. Also, let the objective function be (p+ − p− + 10 · AliceWon). Intuitively, this means that winning the rock-paper-scissors game is considered to have an additional value of 10, other than the spending and earnings. The idea behind this is similar to the case with chess tournaments, in which players not only win a prize, but can also use their wins to achieve better "ratings", so winning has extra utility.

A common bug in writing rock-paper-scissors is allowing the parties to move sequentially, rather than concurrently [29]. If parties can move sequentially and the issuer moves after Bob, then she can ensure a utility of 10, i.e. her worst-case expected reward is 10. However, in the correct implementation as in Fig. 2, the best strategy for both players is to bid 0 and then Alice can win the game with probability 1/3 by choosing each of the three options with equal probability. Hence, her worst-case expected reward is 10/3.

**Auction.** Consider an open auction, in which during a fixed time interval everyone is allowed to bid for the good being sold and everyone can see others' bids. When the bidding period ends a winner emerges and every other participant can get their money back. Let the variable HighestBid store the value of the highest bid made at the auction. Then for a party p, one can define the objective as:

$$(p^{+} - p^{-} + (\mathsf{Winner=} p) \times \mathsf{HigbestBid}.)$$

This is of course assuming that the good being sold is worth precisely as much as the highest bid. A correctly written auction should return a value of 0 to every participant, because those who lose the auction must get their money back and the party that wins pays precisely the highest bid. The contract in Fig. 3 (left) is an implementation of such an auction. However, it has a slight problem. The function bid allows the winner to reduce her bid. This bug is fixed in the contract on the right.

**Fig. 3.** A buggy auction contract (left) and its fixed version (right).

**Three-Way Lottery.** Consider a three-party lottery contract issued by a party p. The other two players can sign up by buying tickets worth 1 unit each. Then each of the players is supposed to randomly and uniformly choose a nonce. A combination of these nonces produces the winner with equal probability for all three parties. If a person does not make a choice or pay the fees, she will certainly lose the lottery. The rules are such that if the other two parties choose the same nonce, which is supposed to happen with probability 1 3 , then the issuer wins. Otherwise the winner is chosen according to the parity of sum of nonces. This gives everyone a winning probability of 1 3 if all sides play uniformly at random. However, even if one of the sides refuses to play uniformly at random, the resulting probabilities of winning stays the same because each side's probability of winning is independent of her own choice assuming that others are playing randomly. We assume that the issuer p has objective p+ −p−. This is because the winner can take other players' money. In a bug-free contract we will expect the value of this objective to be 0, given that winning has a probability of 1 3 . However, the bug here is due to the fact that other parties can collude. For example, the same person might register as both players and then opt for different nonces. This will ensure that the issuer loses. The bug can be solved by ensuring one's probability of winning is 1 3 if she honestly plays uniformly at random, no matter what other parties do. For more details about this contract see [19].

**Token Sale.** Consider a contract that sells *tokens* modeling some aspect of the real world, e.g. shares in a company. At first anyone can buy tokens at a fixed price of 1 unit per token. However, there are a limited number of tokens available and at most 1000 of them are meant to be sold. The tokens can then be transferred between parties, which is the subject of our next example. For now, Fig. 4 (left) is an implementation of the selling phase. However, there is a big problem here. The problem is that one can buy any number of tokens as long as there is at least one token remaining. For example, one might first buy 999 tokens and then buy another 1000. If we analyze the contract from the point of view of a solo party p with objective balance[p], then it must be capped by 1000 in a bug-free contract, while the process described above leads to a value of 1999. The fixed contract is in Fig. 4 (right). This bug is inspired by a very similar real-world bug described in [52].

**Token Transfer.** Consider the same bug-free token sale as in the previous example, we now add a function for transferring tokens. An owner can choose a recipient and an amount less than or equal to her balance and transfer that many tokens to the recipient. Figure 5 (left) is an implementation of this concept. Taking the same approach and objective as above, we expect a similar result. However, there is again an important bug in this code. What happens if a party transfers tokens to herself? She gets free extra tokens! This has been fixed in the contract on the right. This example models a real-world bug as in [42].

**Fig. 4.** A buggy token sale (left) and its fixed version (right).

**Translation to Solidity.** All aspects of our programming language are already present in Solidity, except for the global clock and concurrent interactions. The global clock can be modeled by the number of the current block in the blockchain and concurrent interactions can be implemented using commitment schemes. For more details see [19].

### **4 Bounded Analysis and Games**

Since smart contracts can be easily described in our programming language, and programs in our programming language can be translated to Solidity, the

**Fig. 5.** A buggy transfer function (left) and its fixed version (right).

main aim to automatically compute values of contracts (i.e., compute guaranteed payoff for parties). In this section, we introduce the bounded analysis problem for our programming language framework, and present concurrent games which is the underlying mathematical framework for the bounded analysis problem.

#### **4.1 Bounded Analysis**

As is standard in verification, we consider the bounded analysis problem, where the number of parties and the number of function calls are bounded. In standard program analysis, bugs are often detected with a small number of processes, or a small number of context switches between concurrent threads. In the context of smart contracts, we analogously assume that the number of parties and function calls are bounded.

*Contracts with Bounded Number of Parties and Function Calls.* Formally, a contract with bounded number of parties and function calls is as follows:

closely resembles real-life contracts in which one's ability to call many functions is limited by the capacity of a block in the blockchain, given that the block must save all messages.

### **4.2 Concurrent Games**

The programming language framework we consider has interacting agents that act simultaneously, and we have the program state. We present the mathematical framework of concurrent games, which are games played on finite state spaces with concurrent interaction between the players.

*Concurrent Game Structures.* A concurrent two-player game structure is a tuple G = (S, s0, A, Γ1, Γ2, δ), where S is a finite set of states, s0 ∈ S is the start state, A is a finite set of actions, Γ1, Γ2 : S → 2A \ ∅ such that Γi assigns to each state s ∈ S, a non-empty set Γi(s) ⊆ A of actions available to player i at s, and finally δ : S × A × A → S is a transition function that assigns to every state s ∈ S and action pair a1 ∈ Γ1(s), a2 ∈ Γ2(s) a successor state δ(s, a1, a2) ∈ S.

*Plays and Histories.* The game starts at state s0. At each state si ∈ S, player 1 chooses an action ai 1 ∈ Γ1(si) and player 2 chooses an action ai 2 ∈ Γ2(si). The choices are made simultaneously and independently. The game subsequently transitions to the new state si+1 = δ(si, a1, a2) and the same process continues. This leads to an infinite sequence of tuples p = si, ai 1, ai 2 ∞ i=0 which is called a *play* of the game. We denote the set of all plays by *P*. Every finite prefix p[..r] := (s0, a0 1, a0 2),(s1, a1 1, a1 2),...,(sr, ar 1, ar 2) of a play is called a *history* and the set of all histories is denoted by *H* . If h = p[..r] is a history, we denote the last state appearing according to h, i.e. sr+1 = δ(sr, ar 1, ar 2), by *last*(h). We also define p[.. − 1] as the empty history.

*Strategies and Mixed Strategies.* A strategy is a recipe that describes for a player the action to play given the current game history. Formally, a strategy ϕi for player i is a function ϕi : *H* → A, such that ϕi(h) ∈ Γi(*last*(h)). A pair ϕ = (ϕ1, ϕ2) of strategies for the two players is called a strategy profile. Each such ϕ induces a unique play. A mixed strategy σi : *H* → Δ(A) for player i given the history of the game. Intuitively, such a strategy suggests a distribution of actions to player i at each step and then she plays one of them randomly according to that distribution. Of course it must be the case that Supp(σi(h)) ⊆ Γi(*last*(h)). A pair σ = (σ1, σ2) of mixed strategies for the two players is called a mixed strategy profile. Note that mixed strategies generalize strategies with randomization. Every mixed strategy profile σ = (σ1, σ2) induces a unique probability measure on the set of plays, which is denoted as Probσ[·], and the associated expectation measure is denoted by Eσ[·].

*State and History Utilities.* In a game structure G, a state utility function u for player 1 is of the form u : S → R. Intuitively, this means that when the game enters state s, player 1 receives a reward of u(s). State utilities can be extended to history utilities. We define the utility of a history to be the sum of utilities of all the states included in that history. Formally, if h = si, ai 1, ai 2 r i=0, then u(h) = r i=0 u(si). Given a play p ∈ *P*, we denote the utility of its prefix of length L by uL(p).

*Games.* A game is a pair (G, u) where G is a game structure and u is a utility function for player 1. We assume that player 1 is trying to maximize u, while player 2's goal is to minimize it.

*Values.* The L-step finite-horizon value of a game (G, u) is defined as

$$\text{vol}\_{\mathsf{L}}(G, u) := \sup\_{\sigma\_1} \inf\_{\sigma\_2} \mathbb{E}^{(\sigma\_1, \sigma\_2)} \left[ u\_{\mathsf{L}}(p) \right], \tag{1}$$

where σi iterates over all possible mixed strategies of player i. This models the fact that player 1 is trying to maximize the utility in the first L steps of the run, while player 2 is minimizing it. The values of games can be computed using the value-iteration algorithm or dynamic programming, which is standard. A more detailed overview of the algorithms for games is provided in [19].

*Remark 2.* Note that in (1), limiting player 2 to pure strategies does not change the value of the game. Hence, we can assume that player 2 is an arbitrarily powerful nondeterministic adversary and get the exact same results.

#### **4.3 Translating Contracts to Games**

The translation from bounded smart contracts to games is straightforward, where the states of the concurrent game encodes the states of the contract. Correspondences between objects in the contract and game are as follows: (a) moves in contracts with actions in games; (b) run prefixes in contracts with histories in games; (c) runs in contracts with plays in games; and (d) policies (resp., randomized policies) in contracts with strategies (resp., mixed strategies) in games. Note that since all runs of the bounded contract are finite and have a limited length, we can apply finite horizon analysis to the resulting game, where L is the maximal length of a run in the contract. This gives us the following theorem:

**Theorem 1 (Correspondence).** *Given a bounded contract* Ck *for a party* p *with objective* o*, a concurrent game can be constructed such that value of this game,* υL(G, u)*, is equal to the value of the bounded contract,* V(Ck, o, p)*.*

For details of the translation of smart contracts to games and proof of the theorem above see [19].

*Remark 3.* In standard programming languages, there are no parties to interact and hence the underlying mathematical models are graphs. In contrast, for smart contracts programming languages, where parties interact in a game-like manner, we have to consider games as the mathematical basis of our analysis.

### **5 Abstraction for Quantitative Concurrent Games**

Abstraction is a key technique to handle large-scale systems. In the previous section we described that smart contracts can be translated to games, but due to state-space explosion (since we allow integer variables), the resulting state space of the game is huge. Hence, we need techniques for abstraction, as well as refinement of abstraction, for concurrent games with quantitative utilities. In this section we present such abstraction refinement for quantitative concurrent games, which is our main technical contribution in this paper. We show the soundness of our approach and its completeness in the limit. Then, we introduce a specific method of abstraction, called interval abstraction, which we apply to the games obtained from contracts and show that soundness and refinement are inherited from the general case. We also provide a heuristic for faster refining of interval abstractions for games obtained from contracts.

### **5.1 Abstraction for Quantitative Concurrent Games**

Abstraction considers a partition of the state space, and reduces the number of states by taking each partition set as a state. In case of transition systems (or graphs) the standard technique is to consider existential (or universal) abstraction to define transitions between the partition sets. However, for game-theoretic interactions such abstraction ideas are not enough. We now describe the key intuition for abstraction in concurrent games with quantitative objectives and formalize it. We also provide a simple example for illustration.

*Abstraction Idea and Key Intuition.* In an abstraction the state space of the game (G, u) is partitioned into several abstract states, where an abstract state represents a set of states of the original game. Intuitively, an abstract state represents a set of similar states of the original game. Given an abstraction our goal is to define two games that can provide lower and upper bound on the value of the original game. This leads to the concepts of lower and upper abstraction.

Informally, the lower abstraction gives more power to the adversary, player 2, whereas the upper abstraction is favorable to player 1.

*General Abstraction for Concurrent Games.* Given a game (G, u) consisting of a game structure G = (S, s0, A, Γ1, Γ2, δ) and a utility function u, and a partition Π of S, the lower and upper abstractions, (G↓ = (Sa, sa 0, Aa, Γ↓ 1 , Γ↓ 2 , δ↓), u↓) and (G↑ = (Sa, sa 0, Aa, Γ↑ 1 , Γ↑ 2 , δ↑), u↑), of (G, u) with respect to Π are defined as:

Given a partition Π of S, either (i) there is no lower or upper abstraction corresponding to it because it puts states with different sets of available actions together; or (ii) there is a unique lower and upper abstraction pair. Hence we will refer to the unique abstracted pair of games by specifying Π only.

*Remark 4.* Dummy states are introduced for conceptual clarity in explaining the ideas because in lower abstraction all choices are assigned to player 2 and upper abstraction to player 1. However, in practice, there is no need to create them, as the choices can be allowed to the respective players in the predecessor state.

*Example.* Figure 6 (left) shows a concurrent game with (G, u) with 4 states. The utilities are denoted in red. The edges correspond to transitions in δ and each edge is labeled with its corresponding action pair. Here A = {a, b}, Γ1(s0) = Γ2(s0) = Γ2(s1) = Γ1(s2) = Γ2(s2) = Γ2(s3) = A and Γ1(s1) = Γ1(s3) = {a}. Given that action sets for s0 and s2 are equal, we can create abstracted games using the partition Π = {π0, π1, π2} where π1 = {s0, s2} and other sets are singletons. The resulting game structure is depicted in Fig. 6 (center). Dummy states are shown by circles and whenever a play reaches a dummy state in G↓, player 2 chooses which red edge should be taken. Conversely, in G↑ player 1 makes this choice. Also, u↑(π0) = max{u(s0), u(s2)} = 10, u↓(π0) = min{u(s0), u(s2)} = 0

**Fig. 6.** An example concurrent game (left), abstraction process (center) and the corresponding *G*↓ without dummy states (right).

and u↑(π1)u↓(π1) = u(s1) = 10, u↑(π2) = u↓(π2) = u(s3) = 0. The final abstracted G↓ of the example above, without dummy states, is given in Fig. 6 (right).

### **5.2 Abstraction: Soundness, Refinement, and Completeness in Limit**

For an abstraction we need three key properties: (a) soundness, (b) refinement of the abstraction, and (c) completeness in the limit. The intuitive description is as follows: (a) soundeness requires that the value of the games is between the value of the lower and upper abstraction; (b) refinement requires that if the partition is refined, then the values of lower and upper abstraction becomes closer; and (c) completeness requires that if the partitions are refined enough, then the value of the original game can be approximated. We present each of these results below.

**Soundness.** Soundness means that when we apply abstraction, value of the original game must lie between values of the lower and upper abstractions. Intuitively, this means abstractions must provide us with some interval containing the value of the game. We expect the value of (G↓, u↓) to be less than or equal to the value of the original game because in (G↓, u↓), the utilities are less than in (G, u) and player 2 has more power, given that she can choose which transition to take. Conversely, we expect (G↑, u↑) to have a higher value than (G, u).