*final* if q ∈ F. An interpretation I corresponds to a set of configurations c(I) def = {(q, d1,...,d#(q)) | q ∈ Q, (d1,...,d#(q)) ∈ qI}, called a *cube*. This notation is lifted to sets of configurations in the usual way.

**Definition 1.** *Given a word* w = (a1, ν1)...(an, νn) ∈ Σ[X] ∗ *and a cube* c*, an* execution *of* A = Σ, X, Q, ι, F, Δ *over* w*, starting with* c*, is a forest* T = {T1, T2,...}*, where each* Ti *is a tree labeled with configurations, such that:*

An execution T over w, starting with c, is *accepting* if and only if all paths in T have the same length and the frontier of each tree T ∈ T is labeled with final configurations. If A has an accepting execution over w starting with a cube c ∈ c([[ι]]μ), then A *accepts* w and let L(A) be the set of words accepted by A. For example, consider the automaton A = {a}, {x}, {q0, q1, q2, qf }, q0(0), {qf }, Δ, where Δ is the set: q0(y) a(x) −−→ q1(y + x) ∧ q2(y − x), q1(y) a(x) −−→ q1(y + x) ∨ (y > 0 ∧ qf ) and q2(y) a(x) −−→ q2(y − x) ∨ (y > 0 ∧ qf ). A possible execution tree of this automaton is the following:

The execution tree is not accepting, since its frontier is not labeled with final configurations everywhere. Incidentally, here we have L(A) = ∅, which is proved by our tool in ∼0.5 s on an average machine.

In the rest of this paper, we are concerned with the following problems:

For technical reasons, we address the following problem next: given an automaton A and an input sequence α ∈ Σ∗, does there exists a word w ∈ L(A) such that wΣ = α ? By solving this problem first, we develop the machinery required to prove that first-order alternating automata are closed under complement and, further, set up the ground for developping a practical semi-algorithm for the emptiness problem.

#### **2.1 Path Formulae**

In the upcoming developments it is sometimes more convenient to work with logical formulae defining executions of automata, than with low-level execution forests. For this reason, we first introduce *path formulae* Θ(α), which are formulae defining the executions of an automaton, over words that share a given sequence α of input events. Second, we restrict a path formula Θ(α) to an *acceptance formula* Υ(α), which defines only those executions that are accepting among Θ(α). Consequently, the automaton accepts a word w such that wΣ = α if and only if Υ(α) is satisfiable.

Let A = Σ, X, Q, ι, F, Δ be an automaton for the rest of this section. For any i ∈ N, we denote by Q(i) = {q(i) | q ∈ Q} and X(i) = {x(i) | x ∈ X} the sets of time-stamped predicate symbols and variables, respectively. We also define Q(≤n) def = {q(i) | q ∈ Q, i ∈ [n]} and X(≤n) def = {x(i) | x ∈ X, i ∈ [n]}. For a formula ψ and i ∈ N, we define ψ(i) def = ψ[X(i) /X, Q(i) /Q] the formula in which all input variables and state predicates (and only those symbols) are replaced by their time-stamped counterparts. Moreover, we write q(**y**) for q(y1,...,y#(q)), when no confusion arises.

Given a sequence of input events α = a1 ...an ∈ Σ∗, the *path formula* of α is:

$$\Theta(\alpha) \stackrel{\text{def}}{=} \iota^{(0)} \wedge \bigwedge\_{i=1}^{n} \bigwedge\_{q(\mathbf{y}) \xrightarrow{a\_{i}(X)} \psi \in \Delta} \forall y\_{1} \dots \forall y\_{\#(q)} \; : \; q^{(i-1)}(\mathbf{y}) \to \psi^{(i)} \tag{1}$$

The automaton A, to which Θ(α) refers, will always be clear from the context. To formalize the relation between the low-level configuration-based execution semantics and path formulae, consider a word w = (a1, ν1)...(an, νn) ∈ Σ[X] ∗. Any execution T of A over w has an associated interpretation IT of timestamped predicates Q(≤n) :

IT (*q*(i) ) def = {(*d*1*,...,d*#(*q*)) | (*q, d*1*,...,d*#(*q*)) labels a node on level *i* in T}*,* ∀*q* ∈ *Q* ∀*i* ∈ [*n*]

**Lemma 1.** *Given an automaton* A = Σ, X, Q, ι, F, Δ*, for any word* w = (a1, ν1)...(an, νn)*, we have* [[Θ(wΣ)]]μ wD = {IT | T *is an execution of* A *over* w}*.*

Next, we give a logical characterization of acceptance, relative to a given sequence of input events α ∈ Σ∗. To this end, we constrain the path formula Θ(α) by requiring that only final states of A occur on the last level of the execution. The result is the *acceptance formula* for α:

$$\mathcal{T}(\alpha) \stackrel{\text{def}}{=} \Theta(\alpha) \land \bigwedge\_{q \in Q\backslash F} \forall y\_1 \dots \forall y\_{\#\{q\}} \, \, q^{\langle n \rangle}(\mathbf{y}) \to \bot \tag{2}$$

The top-level universal quantifiers from a subformula ∀y1 ... ∀y#(q) . q(i) (**y**) → ψ of Υ(α) will be referred to as *path quantifiers*, in the following. Notice that path quantifiers are distinct from the transition quantifiers that occur within a formula ψ of a transition rule q(y1,...,y#(q)) a(X) −−−→ ψ of A. The relation between the words accepted by A and the acceptance formula above, is formally captured by the following lemma:

**Lemma 2.** *Given an automaton* A = Σ, X, Q, ι, F, Δ*, for every word* w ∈ Σ[X] ∗*, the following are equivalent: (1) there exists an interpretation* I *such that* I, wD |= Υ(wΣ) *and (2)* w ∈ L(A)*.*

As an immediate consequence, one can decide whether A accepts some word w with a given input sequence wΣ = α, by checking whether Υ(α) is satisfiable. However, unlike non-alternating infinite-state models of computation, such as counter automata (nondeterministic programs with integer variables), the satisfiability query for an acceptance (path) formula falls outside of known decidable theories, supported by standard SMT solvers. There are basically two reasons for this, namely (i) the presence of predicate symbols, and (ii) the non-trivial alternation of quantifiers. To understand this point, consider for example, the decidable theory of Presburger arithmetic [24]. Adding even only one monadic predicate symbol to it yields undecidability in the presence of non-trivial quantifier alternation [10]. On the other hand, the quantifier-free fragment of Presburger arithmetic extended with uninterpreted function symbols is decidable, by a Nelson-Oppen style congruence closure argument [22].

To tackle the problem of deciding satisfiability of Υ(α) formulae, we start from the observation that their form is rather particular, which allows the elimination of path quantifiers and uninterpreted predicate symbols, by a couple of satisfiability-preserving transformations. The result of applying these transformations is a formula with no predicate symbols, whose only quantifiers are those introduced by the transition rules of the automaton. Next, in Sect. 3 we shall assume moreover that the first-order theory of the data sort D (without uninterpreted predicate symbols) has quantifier elimination, providing thus an effective decision procedure.

For the time being, let us formally define the elimination of transition quantifiers and predicate symbols. Let α = a1 ...an be a given sequence of input events and let αi be the prefix a1 ...ai of α, for i ∈ [n], where α0 = . We consider the sequence of formulae Θ(α0),..., Θ(αn) defined as Θ(α0) def = ι (0) and, for all i ∈ [1, n], let Θ(αi) be the conjunction of Θ(αi−1) with all formulae q(i−1)(t1,...,t#(q)) → ψ(i) [t1/y1,...,t#(q)/y#(q)], such that q(i−1)(t1,...,t#(q)) occurs in Θ(αi−1), for some terms t1,...,t#(q). Next, we write Υ(α) for the conjunction of Θ(αn) with all q(n) (t1,...,t#(q)) → ⊥, such that q(n) (t1,...,t#(q)) occurs in Θ(αn), for some q ∈ Q\F. Note that Υ(α) contains no path quantifiers, as required. On the other hand, the scope of the transition quantifiers in Υ(α) exceeds the right-hand side formulae from the transition rules, as shown by the following example.

*Example 1.* Consider the automaton A = {a1, a2}, {x}, {q, qf }, ι, {qf }, Δ, where:

$$\begin{aligned} \iota = \exists z \; . \; z \ge 0 \land q(z) \\ \Delta = \{q(y) \xrightarrow{a\_1(x)} x \ge 0 \land \forall z \; . \; z \le y \to q(x+z), \; q(y) \xrightarrow{a\_2(x)} y < 0 \land q\_f(x+y)\} \end{aligned}$$

For the input event sequence α = a1a2, the acceptance formula is:

$$\begin{array}{l} \mathcal{T}(\alpha) = \exists z\_1 \, \, . \, z\_1 \ge 0 \land q^{(0)}(z\_1) \land \\ \quad \forall y \, . \, q^{(0)}(y) \to [x^{(1)} \ge 0 \land \forall z\_2 \, . \, z\_2 \ge y \to q^{(1)}(x^{(1)} + z\_2)] \land \\ \quad \forall y \, . \, q^{(1)}(y) \to [y < 0 \land q^{(2)}(x^{(2)} + y)] \end{array}$$

The result of eliminating the path quantifiers, in prenex normal form, is shown below:

$$\begin{array}{l} \hat{T}(\alpha) = \exists z\_1 \forall z\_2 \; . \; z\_1 \ge 0 \land q^{(0)}(z\_1) \land \\ \left[ q^{(0)}(z\_1) \to x^{(1)} \ge 0 \land \left( z\_2 \ge z\_1 \to q^{(1)}(x^{(1)} + z\_2) \right) \right] \land \\ \left[ q^{(1)}(x^{(1)} + z\_2) \to x^{(1)} + z\_2 < 0 \land q^{(2)}(x^{(2)} + x^{(1)} + z\_2) \right] \end{array}$$

Notice that the transition quantifiers ∃z1 and ∀z2 from Υ(α) range now over Υ(α). -

**Lemma 3.** *For any input event sequence* α = a1 ...an *and each valuation* ν : X(≤n) → D*, the following hold, for every interpretation* I*: (1) if* I, ν |= Υ(α) *then* I, ν |= Υ(α)*, and (2) if* I, ν |= Υ(α) *there exists an interpretation* J ⊆ I *such that* J, ν |= Υ(α)*.*

Further, we eliminate the predicate atoms from Υ(α), by considering the sequence of formulae Θ(α0) def = ι (0) and Θ(αi) is obtained by substituting each predicate atom q(i−1)(t1,...,t#(q)) in Θ(αi−1) by ψ(i) [t1/y1,...,t#(q)/y#(q)], where q(**y**) ai(X) −−−→ ψ ∈ Δ, for all i ∈ [1, n]. We write Υ(α) for the formula obtained by replacing, in Θ(α), each occurrence of a predicate q(n) , such that q ∈ Q \ F (resp. q ∈ F), by ⊥ (resp. ).

*Example 2* (*Contd. from Example* 1*).* The result of the elimination of predicate atoms from the acceptance formula in Example 1 is shown below:

$$\left| \overline{T}(\alpha) = \exists z\_1 \forall z\_2 \; . \; z\_1 \ge 0 \land \left[ x^{(1)} \ge 0 \land \left( z\_2 \ge z\_1 \to x^{(1)} + z\_2 < 0 \right) \right] \right|$$

Since this formula is unsatisfiable, by Lemma 5 below, no word w with input event sequence wΣ = a1a2 is accepted by the automaton A from Example 1. -

At this point, we prove the formal relation between the satisfiability of the formulae Υ(α) and Υ(α). Since there are no occurrences of predicates in Υ(α), for each valuation ν : X(≤n) → D, there exists an interpretation I such that I, ν |= Υ(α) if and only if J, ν |= Υ(α), for every interpretation J. In this case we omit I and simply write ν |= Υ(α).

**Lemma 4.** *For any input event sequence* α = a1 ...an *and each valuation* ν : X(≤n) → D*, there exists a valuation* I *such that* I, ν |= Υ(α) *if and only if* ν |= Υ(α)*.*

Finally, we define the acceptance of a word with a given input event sequence by means of a quantifier-free formula in which no predicate atom occurs.

**Lemma 5.** *Given an automaton* A = Σ, X, Q, ι, F, Δ*, for every word* w ∈ Σ[X] ∗*, we have* wD |= Υ(wΣ) *if and only if* w ∈ L(A)*.*

#### **2.2 Boolean Closure of First Order Alternating Automata**

Given a positive formula φ, we define the *dual* formula φ∼ recursively as follows:

$$\begin{array}{llll} \left(\phi\_{1}\vee\phi\_{2}\right)^{\sim} \stackrel{\text{def}}{=} \phi\_{1}\stackrel{\sim}{}\wedge\phi\_{2} & \qquad \left(\phi\_{1}\wedge\phi\_{2}\right)^{\sim} \stackrel{\text{def}}{=} \phi\_{1}\stackrel{\sim}{}\vee\phi\_{2} & \qquad \left(t=s\right)^{\sim} \stackrel{\text{def}}{=} t \neq s\\ \left(\exists x\,\,.\,\phi\_{1}\right)^{\sim} \stackrel{\text{def}}{=} \forall x\,\,.\,\phi\_{1} & \qquad \left(\forall x\,\,.\,\phi\_{1}\right)^{\sim} \stackrel{\text{def}}{=} \exists x\,\,.\,\phi\_{1} & \qquad \left(t\neq s\right)^{\sim} \stackrel{\text{def}}{=} t = s\\ & & \qquad q\left(x\_{1},\ldots,x\_{\#\left(q\right)}\right)^{\sim} \stackrel{\text{def}}{=} q\left(x\_{1},\ldots,x\_{\#\left(q\right)}\right) \end{array}$$

The following theorem shows closure of automata under all boolean operations. Note that it is sufficient to show closure under intersection and negation because L(A1) ∪ L(A2) is the complement of the language Lc(A1) ∩ Lc(A2), for any two automata A1 and A2 with the same input event alphabet and set of input variables.

**Theorem 1.** *Given automata* Ai = Σ, X, Qi, ιi, Fi, Δi*, for* i = 1, 2*, such that* Q1 ∩ Q2 = ∅*, the following hold:*

*1.* L(A∩) = L(A1) ∩ L(A2)*, where* A∩ = Σ, X, Q1 ∪ Q2, ι1 ∧ ι2, F1 ∪ F2, Δ1 ∪ Δ2*,*

$$\begin{array}{l} \text{2. } \mathcal{L}(\overline{\mathcal{R}\_{i}}) = \Sigma[X]^{\*} \mid \mathcal{L}(\mathcal{R}\_{i}), \text{ where } \overline{\mathcal{R}\_{i}} = \langle \Sigma, X, Q\_{i}, \iota^{\sim}, Q\_{i} \mid F\_{i}, \Delta\_{i}^{\sim} \rangle \text{ and } \Delta\_{i}^{\sim} = \langle q(\mathbf{y}) \xrightarrow{a(X)} \psi^{\sim} \mid q(\mathbf{y}) \xrightarrow{a(X)} \psi \in \Delta\_{i} \rangle, \text{ for } i = 1, 2. \end{array}$$

*Moreover,* |A∩| = O(|A1| + |A2|) *and* |Ai| = O(|Ai|)*, for* i = 1, 2*.*

#### **3 The Emptiness Problem**

The emptiness problem is undecidable even for automata with predicates of arity two, whose transition rules use only equalities and disequalities, having no transition quantifiers [6]. Since even such simple classes of alternating automata have no general decision procedure for emptiness, we use an abstraction-refinement semi-algorithm based on *lazy annotation* [20,21]. In a nutshell, a lazy annotation procedure systematically explores the set of finite input event sequences searching for an accepting execution. For an input sequence, if the path formula is satisfiable, we compute a word in the language of the automaton, from the model of the path formula. Otherwise, i.e. the sequence is *spurious*, the search backtracks and each position in the sequence is annotated with an interpolant, thus marking the sequence as infeasible. The semi-algorithm uses moreover a coverage relation between sequences, ensuring that the continuations of already covered sequences are never explored. Sometimes this coverage relation provides a sound termination argument, in case when the automaton is empty.

For two input event sequences α, β ∈ Σ∗, we say that α is a prefix of β, written α β, if α = βγ for some sequence γ ∈ Σ∗. A set S of sequences is *prefix-closed* if for each α ∈ S, if β α then β ∈ S, and *complete* if for each α ∈ S, there exists a ∈ Σ such that αa ∈ S if and only if αb ∈ S for all b ∈ Σ. A prefix-closed set is the backbone of a tree whose edges are labeled with input events. If the set is, moreover, complete, then every node of the tree has either zero successors, in which case it is called a *leaf*, or it has a successor edge labeled with a for each input event a ∈ Σ.

**Definition 2.** *An* unfolding *of an automaton* A = Σ, X, Q, ι, F, Δ *is a finite partial mapping* U : Σ∗ *fin* Form+(Q, ∅)*, whose domain* dom(U) *is a finite prefix-closed complete set, such that* U( ) = ι*, and for each sequence* αa ∈ dom(U)*, such that* α ∈ Σ∗ *and* a ∈ Σ*:*

$$U(\alpha)^{(0)} \wedge \bigwedge\_{q(\mathbf{y}) \xrightarrow{a(X)} \psi} \forall y\_1 \dots \forall y\_{\#q} \,\,\, q^{(0)}(\mathbf{y}) \to \psi^{(1)} \,\, \vert = U(\alpha a)^{(1)}$$

*A path* α *is* safe *in* U *if and only if* U(α) ∧ q∈Q\F ∀y1 ... ∀y#(q) . q(**y**) → ⊥ *is unsatisfiable. The unfolding* U *is safe if and only if every path in* dom(U) *is safe in* U*.*

Lazy annotation semi-algorithms [20,21] build unfoldings of automata trying to discover counterexamples for emptiness. If the automaton A in question is non-empty, a systematic enumeration of the input event sequences2 from Σ∗ will suffice to discover a word w ∈ L(A), provided that the first-order theory of the data domain D is decidable (Lemma 2). However, if L(A) = ∅, the enumeration of input event sequences may, in principle, run forever. The typical way of fighting this divergence problem is to define a *coverage* relation between the nodes of the unfolding tree.

**Definition 3.** *Given an unfolding* U *of an automaton* A = Σ, X, Q, ι, F, Δ *a node* α ∈ dom(U) *is* covered *by another node* β ∈ dom(U)*, denoted* α β*, if and only if there exists a node* α α *such that* U(α ) |= U(β)*. Moreover,* U *is* closed *if and only if every leaf from* dom(U) *is covered by an uncovered node.*

A lazy annotation semi-algorithm will stop and report emptiness provided that it succeeds in building a closed and safe unfolding of the automaton. Notice that, by Definition 3, for any three nodes of an unfolding U, say α, β, γ ∈ dom(U), if α ≺ β and α γ, then β γ as well. As we show next (Theorem 2), there is no need to expand covered nodes, because, intuitively, there exists a word w ∈ L(A) such that α wΣ and α γ only if there exists another word u ∈ L(A) such that γ uΣ. Hence, exploring only those input event sequences that are continuations of γ (and ignoring those of α) suffices in order to find a counterexample for emptiness, if one exists.

An unfolding node α ∈ dom(U) is said to be *spurious* if and only if Υ(α) is unsatisfiable. In this case, we change (refine) the labels of (some of the) prefixes of α (and that of α), such that U(α) becomes ⊥, thus indicating that there is no real execution of the automaton along that input event sequence. As a result of the change of labels, if a node γ α used to cover another node from dom(U), it might not cover it with the new label. Therefore, the coverage relation has to be recomputed after each refinement of the labeling. The semi-algorithm stops when (and if) a safe complete unfolding has been found.

**Theorem 2.** *If an automaton* A *has a nonempty safe closed unfolding then* L(A) = ∅*.*

2 For instance, using breadth-first search.

#### **Algorithm 1.** IMPACT-based Semi-algorithm for First Order Alternating Automata

**input**: a first order alternating automaton A = Σ, X, Q, ι, F, Δ **output**: if L(A) = ∅, or word w ∈ L(A), otherwise **data structures**: WorkList and unfolding tree U = N,E, r, U, ✁, where: – N is a set of nodes, – E ⊆ N × Σ × N is a set of edges labeled by input events, – U : N → Form+(Q, ∅) is a labeling of nodes with positive sentences – ✁ ⊆ N × N is a coverage relation, **initially** WorkList = {r} and N = E = U = ✁ = ∅. 1: **while** WorkList = ∅ **do** 2: dequeue n from WorkList 3: N ← N ∪ {n} 4: let α(n) be a1,...,a*k* 5: **if** Υ(α)(X(1),...,X(k) ) is satisfiable **then** counterexample is feasible 6: get model ν of Υ(α)(X(1),...,X(k) ) 7: **return** w = (a1, ν(X(1))) ... (a*k*, ν(X(k) )) w ∈ L(A) by construction 8: **else** spurious counterexample 9: let (I0,...,I*k*) be a GLI for α 10: b ← ⊥ 11: **for** i = 0,...,k **do** 12: **if** U(n*i*) |= I*i* **then** 13: *Uncover* ← {m ∈ N | (m, n*i*) ∈ ✁} 14: ✁ ← ✁ \ {(m, n*i*) | m ∈ *Uncover*} uncover the nodes covered by n*i* 15: **for** m ∈ *Uncover* such that m is a leaf of U **do** 16: enqueue m into WorkList reactivate uncovered leaves 17: U(n*i*) ← U(n*i*) ∧ J*i* strenghten the label of n*i* (Lemma 7) 18: **if** ¬b **then** 19: b ← Close(n*i*) 20: **if** n is not covered **then** 21: **for** a ∈ Σ **do** expand n 22: let s be a fresh node and e = (n, a, s) be a new edge 23: E ← E ∪ {e} 24: U ← U ∪ {(s, )} 25: enqueue s into WorkList 26: **return** 27: **function** Close(x) **returns** B 28: **for** y ∈ N such that α(y) ≺∗ α(x) **do** 29: **if** U(x) |= U(y) **then** 30: ✁ ← [✁ \ {(p, q) ∈ ✁ | q is x or a successor of x}] ∪ {(x, y)} 31: **return** 32: **return** ⊥

We describe the semi-algorithm used to check emptiness of first-order alternating automata. The execution of Algorithm 1 consists of three phases, corresponding to the Close, Refine and Expand of the original IMPACT procedure [20]. Let n be a node removed from the worklist at line 2 and let α(n) be the input sequence labeling the path from the root node to n. If Υ(α(n)) is satisfiable, the sequence α(n) is feasible, in which case a model of Υ(α(n)) is obtained and a word w ∈ L(A) is returned. Otherwise, α(n) is an infeasible input sequence and the procedure enters the refinement phase (lines 9–19). The GLI for α(n) is used to strenghten the labels of all the ancestors of n, by conjoining the formulae of the interpolant, changed according to Lemma 7, to the existing labels.

In this process, the nodes on the path between r and n, including n, might become eligible for coverage, therefore we attempt to close each ancestor of n that is impacted by the refinement (line 19). Observe that, in this case the call to Close must uncover each node which is covered by a successor of n (line 30 of the Close function). This is required because, due to the over-approximation of the sets of reachable configurations, the covering relation is not transitive, as explained in [20]. If Close adds a covering edge (ni, m) to ✁, it does not have to be called for the successors of ni on this path, which is handled via the boolean flag b. Finally, if n is still uncovered (it has not been previously covered during the refinement phase) we expand n (lines 21–25) by creating a new node for each successor s via the input event a ∈ Σ and inserting it into the worklist.

#### **4 Interpolant Generation**

Typically, when checking the unreachability of a set of program configurations, the interpolants used to annotate the unfolded control structure are assertions about the values of the program variables in a given control state, at a certain step of an execution [20]. Because we consider alternating computation trees (forests), we must distinguish between (i) locality of interpolants w.r.t. a given control state (control locality) and (ii) locality w.r.t. a given time stamp (time locality). In logical terms, *control-local* interpolants are formulae involving a single predicate symbol, whereas *time-local* interpolants involve only predicates q(i) and variables x(i) , for a single i ≥ 0. When considering alternating executions, control-local interpolants are not always enough to prove emptiness, because of the synchronization of several branches of the computation on the same input word. For this reason, the interpolants considered in this paper will never be control-local and we shall use the term *local* to denote time-local interpolants, with no free variables.

First, let us give the formal definition of the class of interpolants we shall work with. Given a formula φ, the *vocabulary* of φ, denoted V(φ) is the set of predicate symbols q ∈ Q(i) and variables x ∈ X(i) , occurring in φ, for some i ≥ 0. For a term t, its vocabulary V(t) is the set of variables that occur in t. Observe that quantified variables and the interpreted function symbols of the data theory3 do not belong to the vocabulary of a formula. By P+(φ) [P−(φ)] we denote the set of predicate symbols that occur in φ under an even [odd] number of negations.

3 E.g., the arithmetic operators of addition and multiplication, when D is the set of integers.

**Definition 4 (**[19]**).** *Given formulae* φ *and* ψ *such that* φ ∧ ψ *is unsatisfiable, a* Lyndon interpolant *is a formula* I *such that* φ |= I*, the formula* I ∧ ψ *is unsatisfiable,* V(I) ⊆ V(φ)∩V(ψ)*,* P+(I) ⊆ P+(φ)∩P+(ψ) *and* P−(I) ⊆ P−(φ)∩ P−(ψ)*.*

In the rest of this section, fix an automaton A = Σ, X, Q, ι, F, Δ. The following definition generalizes interpolants from unsatisfiable conjunctions to input sequences:

**Definition 5.** *Given a sequence of input events* α = a1 ...an ∈ Σ∗*, a* generalized Lyndon interpolant (GLI) *is a sequence* (I0,...,In) *of formulae such that, for all* k ∈ [n − 1]*, the following hold: (1)* P−(Ik) = ∅*, (2)* ι (0) |= I0*,* Ik ∧ q(**y**) ai(X) −−−→ψ∈Δ ∀y1 ... ∀y#(q) . q(k) (**y**) → ψ(k+1) |= Ik+1 *and (3)* In ∧ q∈Q\F ∀y1 ... ∀y#(q) . q(**y**) → ⊥ *is unsatisfiable. Moreover, the GLI is* local *if and only if* V(Ik) ⊆ Q(k) *, for all* k ∈ [n]*.*

The following proposition states the existence of local GLI for the theories in which Lyndon's Interpolation Theorem holds.

**Proposition 1.** *If there exists a Lyndon interpolant for any two formulae* φ *and* ψ*, in the first-order theory of data with uninterpreted predicate symbols, such that* φ∧ψ *is unsatisfiable, then any sequence of input events* α = a1 ...an ∈ Σ∗*, such that* Υ(α) *is unsatisfiable, has a local GLI* (I0,...,In)*.*

A problematic point of the above proposition is that the existence of Lyndon interpolants (Definition 4) is proved in principle, but the proof is nonconstructive. In other words, the proof of Proposition 1 does not yield an algorithm for computing GLIs, for the following reason. Building an interpolant for an unsatisfiable conjunction of formulae φ ∧ ψ is typically the job of the decision procedure that proves the unsatisfiability and, in general, there is no such procedure, when φ and ψ contain predicates and have non-trivial quantifier alternation. In this case, some provers use instantiation heuristics for the universal quantifiers that are sufficient for proving unsatisfiability, however these heuristics are not always suitable for interpolant generation. Consequently, from now on, we assume the existence of an effective Lyndon interpolation procedure only for decidable theories, such as the quantifier-free linear (integer) arithmetic with uninterpreted functions (UFLIA, UFLRA, etc.) [26].

This is where the predicate-free path formulae (defined in Sect. 2.1) come into play. Recall that, for a given event sequence α, the automaton A accepts a word w such that wΣ = α if and only if Υ(α) is satisfiable (Lemma 5). Assuming further that the equality and interpreted predicates (e.g. inequalities for integers) atoms from the transition rules of A belong to a decidable first-order theory, such as Presburger arithmetic, Lemma 5 gives us an effective way of checking emptiness of A, relative to a given event sequence. However, this method does not cope well with lazy annotation, because there is no way to extract, from the unsatisfiability proof of Υ(α), the interpolants needed to annotate α. This is because (I) the formula Υ(α), obtained by repeated substitutions loses track of the steps of the execution, and (II) quantifiers that occur nested in Υ(α) make it difficult to write Υ(α) as an unsatisfiable quantifier-free conjunction of formulae from which interpolants are extracted (Definition 4).

The solution we adopt for the first issue (I) consists in partially recovering the time-stamped structure of the acceptance formula Υ(α) using the formula Υ(α), in which only transition quantifiers occur. The second issue (II) is solved under the additional assuption that the theory of the data domain D has *witnessproducing quantifier elimination*. More precisely, we assume that, for each formula ∃x.φ(x), there exists an effectively computable term τ , in which x does not occur, such that ∃x.φ and φ[τ /x] are equisatisfiable. These terms, called *witness terms* in the following, are actual definitions of the Skolem function symbols from the following folklore theorem:

**Theorem 3 (**[3]**).** *Given* Q1x1 ...Qnxn . φ *a first-order sentence, where* Q1,...,Qn ∈ {∃, ∀} *and* φ *is quantifier-free, let* ηi def = fi(y1,...,yki ) *if* Qi = ∀ *and* ηi def = xi *if* Qi = ∃*, where* fi *is a fresh function symbol and* {y1,...,yki } = {xj | j < i, Qj = ∃}*. Then the entailment* Q1x1 ...Qnxn . φ |= φ[η1/x1,...,ηn/xn] *holds.*

Examples of witness-producing quantifier elimination procedures can be found in the literature for e.g. linear integer (real) arithmetic (LIA,LRA), Presburger arithmetic and boolean algebra of sets and Presburger cardinality constraints (BAPA) [18].

Under the assumption that witness terms can be effectively built, we describe the generation of a non-local GLI for a given input event sequence α = a1 ...an. First, we generate successively the acceptance formula Υ(α) and its equisatisfiable forms Υ(α) = Q1x1 ...Qmxm . Φ and Υ(α) = Q1x1 ...Qmxm . Φ, both written in prenex form, with matrices Φ and Φ, respectively. Because we assumed that the first order theory of D has quantifier elimination, the satisfiability problem for Υ(α) is decidable. If Υ(α) is satisfiable, we build a counterexample for emptiness w such that wΣ = α and wD is a satisfying assignment for Υ(α). Otherwise, Υ(α) is unsatisfiable and there exist witness terms τi1 ...τi- , where {i1,...,i} = {j ∈ [1, m] | Qj = ∀}, such that Φ[τi1 /xi1 ,...,τi- /xi- ] is unsatisfiable (Theorem 3). Then it turns out that the formula Φ[τi1 /xi1 ,...,τi- /xi- ], obtained analogously from the matrix of Υ(α), is unsatisfiable as well (Lemma 6 below). Because this latter formula is structured as a conjunction of formulae ι (0) ∧ φ1 ... ∧ φn ∧ ψ, where V(φk) ∩ Q(≤n) ⊆ Q(k−1) ∪ Q(k) and V(ψ) ∩ Q(≤n) ⊆ Q(n) , it is now possible to use an existing interpolation procedure for the quantifier-free theory of D, extended with uninterpreted function symbols, to compute a (not necessarily local) GLI (I0,...,In) such that V(Ik) ∩ Q(≤n) ⊆ Q(k) , for all k ∈ [n].

*Example 3* (*Contd. from Examples* 1 *and* 2*).* The formula Υ(α) (Example 2) is unsatisfiable and let τ2 def = z1 be the witness term for the universally quantified variable z2. Replacing z2 with τ2 (z1) in the matrix of Υ(α) (Example 1) yields the unsatisfiable conjunction below, obtained after trivial simplifications:

$$\begin{array}{c} \left[ z\_1 \ge 0 \land q^{(0)}(z\_1) \right] \land \left[ q^{(0)}(z\_1) \to x^{(1)} \ge 0 \land q^{(1)}(x^{(1)} + z\_1) \right] \land \\\left[ q^{(1)}(x^{(1)} + z\_1) \to x^{(1)} + z\_1 < 0 \land q^{(2)}(x^{(2)} + x^{(1)} + z\_1) \right] \end{array}$$

A non-local GLI for the above conjunction is the sequence of formulae:

$$\{q^{(0)}(z\_1) \land z\_1 \ge 0, \ x^{(1)} \ge 0 \land q^{(1)}(x^{(1)} + z\_1) \land z\_1 \ge 0, \ \bot\}$$

We formalize and prove the correctness for the above construction of nonlocal GLI. A function ξ : N → N is *monotonic* iff for each n<m we have ξ(n) ≤ ξ(m) and *finite-range* iff for each n ∈ N the set {m | ξ(m) = n} is finite. If ξ is finite-range, we denote by ξ−1 max(n) ∈ N the maximal value m such that ξ(m) = n.

**Lemma 6.** *Given a non-empty input event sequence* α = a1 ...an ∈ Σ∗*, such that* Υ(α) *is unsatisfiable, let* Q1x1 ...Qmxm . Φ *be a prenex form of* Υ(α) *and let* ξ : [1, m] → [n] *be a monotonic finite-range function mapping each transition quantifier to the minimal index from the sequence* Θ(α0),..., Θ(αn) *where it occurs. Then one can effectively build:*

Consequently, under two assumptions about the first-order theory of the data domain, namely (i) witness-producing quantifier elimination, and (ii) Lyndon interpolation for the quantifier-free fragment with uninterpreted functions, we developed a generic method that produces GLIs for unfeasible input event sequences. Moreover, each formula in the interpolant refers only to the current predicate symbols, the current and past input variables and the existentially quantified transition variables introduced at the previous steps. The remaining questions are how to use these GLIs to label the sequences in the unfolding of an automaton (Definition 2) and compute coverage (Definition 3) between nodes of the unfolding.

#### **4.1 Unfolding with Non-local Interpolants**

As required by Definition 2, the unfolding U of an automaton A = Σ, X, Q, ι, F, Δ is labeled by formulae U(α) ∈ Form+(Q, ∅), with no free symbols, other than predicate symbols, such that the labeling is compatible with the transition relation of the automaton. Each newly expanded input sequence of A is initially labeled with and the labels are refined using GLIs computed from proofs of spuriousness. The following lemma describes the refinement of the labeling of an input sequence by a non-local GLI:

**Lemma 7.** *Let* U *be an unfolding of an automaton* A = Σ, X, Q, ι, F, Δ *such that* α = a1 ...an ∈ dom(U) *and* (I0,...,In) *is a GLI for* α*. Then the mapping* U : dom(U) → Form+(Q, ∅) *is an unfolding of* A*, where:*

*Moreover,* α *is safe in* U *.*

Observe that, by Lemma 6(2), the set of free variables of a GLI formula Ik consists of (i) variables X(≤k) keeping track of data values seen in the input at some earlier moment in time, and (ii) variables that track past choices made within the transition rules. Basically, it is not important when exactly in the past a certain input has been read or when a choice has been made, because only the relation between the values of these and the current variables determines the future behavior of the automaton. Quantifying these variables existentially does the job of ignoring when exactly in the past these values have been seen. Moreover, the last point of Lemma 7 ensures that the refined path is safe in the new unfolding and will stay safe in all future refinements of this unfolding.

The last ingredient of the lazy annotation semi-algorithm based on unfoldings consist in the implementation of the coverage check, when the unfolding of an automaton is labeled with conjunctions of existentially quantified formulae with predicate symbols, obtained from interpolation. By Definition 3, checking whether a given node α ∈ dom(U) is covered amounts to finding a prefix α α and a node β ∈ dom(U) such that U(α ) |= U(β), or equivalently, the formula U(α ) ∧ ¬U(β) is unsatisfiable. However, the latter formula, in prenex form, has quantifier prefix in the language ∃∗∀∗ and, as previously mentioned, the satisfiability problem for such formulae becomes undecidable when the data theory subsumes Presburger arithmetic [10].

Nevertheless, if we require just a yes/no answer (i.e. not an interpolant) recently developed quantifier instantiation heuristics [25] perform rather well in answering a large number of queries in this class. Observe, moreover, that coverage does not need to rely on a complete decision procedure. If the prover fails in answering the above satisfiability query, then the semi-algorithm assumes that the node is not covered and continues exploring its successors. Failure to compute complete coverage may lead to divergence (non-termination) and ultimately, to failure to prove emptiness, but does not affect the soundness of the semi-algorithm (real counterexamples will still be found).

#### **5 Experimental Results**

We have implemented a version of the IMPACT semi-algorithm [20] in a prototype tool, avaliable online [8]. The tool is written in Java and uses the Z3 SMT solver [27], via the JavaSMT interface [15], for spuriousness and coverage

 **1.** Experiments with First Order Alternating Automata

**Table**

queries and also for interpolant generation. Table 1 reports the size of the input automaton in bytes, the numbers of Predicates, Variables and Transitions, the result of emptiness check, the number of Expanded and Visited Nodes during the unfolding and the Time in miliseconds. The experiments were carried out on a MacOS x64 - 1.3 GHz Intel Core i5 - 8 GB 1867 MHz LPDDR3 machine.

The test cases shown in Table 1, come from several sources, namely predicate automata models (\*.pa) [6,7] available online [23], timed automata inclusion problems (abp.ada, train.ada, rr-crossing.foada), array logic entailments (array rotation.ada, array simple.ada, array shift.ada) and hardware circuit verification (hw1.ada, hw2.ada), initially considered in [13], with the restriction that local variables are made visible in the input. The train-simpleN. foada and fischer-mutexN. foada examples are parametric verification problems in which one checks inclusions of the form N i=1 L(Ai) ⊆ L(B), where Ai is the i-th copy of the template automaton.

The advantage of using FOADA over the INCLUDER [12] tool from [13] is the possibility of having automata over infinite alphabets with local variables, whose values are not visible in the input. In particular, this is essential for checking inclusion of timed automata that use internal clocks to control the computation.

#### **6 Conclusions**

We present first-order alternating automata, a model of computation that generalizes classical boolean alternating automata to first-order theories. Due to their expressivity, first-order alternating automata are closed under union, intersection and complement. However the emptiness problem is undecidable even in the most simple case, of the quantifier-free theory of equality with uninterpreted predicate symbols. We deal with the emptiness problem by developping a practical semi-algorithm that always terminates, when the automaton is not empty. In case of emptiness, termination of the semi-algorithm occurs in most practical test cases, as shown by a number of experiments.

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

## **Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors**

Martin Jon´aˇs(B) and Jan Strejˇcek

Masaryk University, Brno, Czech Republic<EMAIL_ADDRESS>
**Abstract.** We present the first stable release of our tool Q3B for deciding satisfiability of quantified bit-vector formulas. Unlike other state-ofthe-art solvers for this problem, Q3B is based on translation of a formula to a bdd that represents models of the formula. The tool also employs advanced formula simplifications and approximations by effective bitwidth reduction and by abstraction of bit-vector operations. The paper focuses on the architecture and implementation aspects of the tool, and provides a brief experimental comparison with its competitors.

#### **1 Introduction**

Advances in solving formula *satisfiability modulo theories* (smt) achieved during the last few decades enabled significant progress and practical applications in the area of automated analysis, testing, and verification of various systems. In the case of software and hardware systems, the most relevant theory is the *theory of fixed-sized bit-vectors*, as these systems work with inputs expressed as bitvectors (i.e., sequences of bits) and perform bitwise and arithmetic operations on bit-vectors. The quantifier-free fragment of this theory is supported by many general-purpose smt solvers, such as CVC4 [1], MathSAT [7], Yices [10], or Z3 [9] and also by several dedicated solvers, such as Boolector [21] or STP [12]. However, there are some use-cases where quantifier-free formulas are not natural or expressive enough. For example, formulas containing quantifiers arise naturally when expressing loop invariants, ranking functions, loop summaries, or when checking equivalence of two symbolically described sets of states [8,13,17,18,24]. In the following, we focus on smt solvers for *quantified* bit-vector formulas. In particular, this paper describes the state-of-the-art smt solver Q3B including its implementation and the inner workings.

Solving of quantified bit-vector formulas was first supported by Z3 in 2013 [25] and for a limited set of *exists/forall* formulas with only a single quantifier alternation by Yices in 2015 [11]. Both of these solvers decide quantified formulas by *quantifier instantiation*, in which universally quantified variables in the Skolemized formula are repeatedly instantiated by ground terms until the resulting quantifier-free formula is unsatisfiable or a model of the original formula is found.

c The Author(s) 2019 I. Dillig and S. Tasiran (Eds.): CAV 2019, LNCS 11562, pp. 64–73, 2019. https://doi.org/10.1007/978-3-030-25543-5\_4

This work has been supported by Czech Science Foundation, grant GA18-02177S.

In 2016, we proposed a different approach for solving quantified bit-vector formulas: by using binary decision diagrams (bdds) and approximations [14]. For evaluation of this approach, we implemented an experimental smt solver called Q3B, which outperformed both Z3 and Yices. Next solver that was able to solve quantified bit-vector formulas was Boolector in 2017, using also an approach based on quantifier instantiation [22]. Unlike Z3, in which the universally quantified variables are instantiated only by constants or subterms of the original formula, Boolector uses a counterexample-guided synthesis approach, in which a suitable ground term for instantiation is synthesized based on the defined grammar. Thanks to this, Boolector was able to outperform Q3B and Z3 on certain classes of formulas. More recently, in 2018, support of quantified bit-vector formulas has also been implemented into CVC4 [20]. The approach of CVC4 is also based on quantifier instantiation, but instead of synthesizing terms given by the grammar as Boolector, CVC4 uses predetermined rules based on invertibility conditions, which directly give terms that can prune many spurious models without using potentially expensive counterexample-guided synthesis. The authors of CVC4 have shown that this approach outperforms Z3, CVC4, and the original Q3B. However, Q3B has been substantially improved since the original experimental version. In 2017, we extended it with simplifications of quantified bitvector formulas using unconstrained variables [15]. Further, in 2018, we added the experimental implementation of abstractions of bit-vector operations [16]. With these techniques, Q3B is able to decide more formulas than Z3, Boolector, and CVC4. Besides the theoretical improvements, Q3B was also improved in terms of stability, ease of use, technical parts of the implementation, and compliance with the smt-lib standard. This tool paper presents the result of these improvements: Q3B 1.0, the first stable version of Q3B.

We briefly summarize the smt solving approach of Q3B. As in most of modern smt solvers, the input formula is first simplified using satisfiability-preserving transformations that may reduce the size and complexity of the formula. The simplified formula is then converted to a binary decision diagram (bdd) that represents all assignments satisfying the formula, i.e., the *models* of the formula. If the bdd represents at least one model, we say that the bdd is *satisfiable* and it implies satisfiability of the formula. If the bdd represents the empty set of models, we say that it is *unsatisfiable* and so is the formula. Unfortunately, there are formulas for which the corresponding bdd (or some of the intermediate bdds that appear during its computation) is necessarily exponential in the number of bits in the formula. For example, this is the case for formulas that contain multiplication of two bit-vector variables [5]. To be able to deal with such formulas, Q3B computes in parallel also bdds underapproximating and overapproximating the original set of models, i.e., bdds representing subsets and supersets of the original set of models, respectively. The approximating bdds may be much smaller in size than the precise bdd, especially if the approximation is very rough. Still, they can be used to decide satisfiability of the original formula. If an overapproximating bdd is unsatisfiable, the original formula is also unsatisfiable. If the overapproximating bdd is satisfiable, we take one of its models, i.e., an assignment to the top-level existential variables of the formula, and check whether it is a model of the original formula. If the answer is positive, the original formula is satisfiable. In the other case, we build a more precise overapproximating bdd. Underapproximating bdds are utilized analogously. The only difference is that for unsatisfiable underapproximating bdd, we check the validity of a countermodel, i.e., an assignment to the top-level universal variables that makes the formula unsatisfiable. The approach is depicted in Fig. 1.

**Fig. 1.** High-level overview of the smt solving approach used by Q3B. The three shaded areas are executed in parallel and the first result is returned.

Q3B currently supports two ways of computing the approximating bdds from the input formula. First of these are *variable bit-width approximations* in which the *effective bit-width* of some variables is reduced. In other words, some of the variables are represented by fewer bits and the rest of the bits is set to zero bits, one bits, or the sign bit of the reduced variable. This approach was originally used by the smt solvers uclid [6] and Boolector [21]. Q3B extends this approach to quantified formulas: if bit-widths of only existentially quantified variables are reduced, the resulting bdd is underapproximating; if bit-widths of only universally quantified variables are reduced, the resulting bdd is overapproximating. The second way to obtain an approximation is *bit-vector operation abstraction* [16], during which the individual bit-vector operations may not compute all bits of the result, but produce some *do-not-know bits* if the resulting bdds would exceed a given number of nodes. An underapproximating bdd then represents assignments that satisfy the formula for all possible values of these do-not-know bits. Analogously, an overapproximating bdd represents all assignments that satisfy the formula for some value of the do-not-know bits. Q3B also supports a combination of these two methods, in which both the effective bit-with of variables is reduced and the limit on the size of bdds is imposed. During an approximation refinement, either the effective bit-width or the size limit is increased, based on the detected cause of the imprecision.

**Fig. 2.** Architecture of Q3B. Components in the shaded box are parts of Q3B, the other components are external.

#### **2 Architecture**

This section describes the internal architecture of Q3B. The overall structure including internal and external components and the interactions between them is depicted in Fig. 2. We explain the purpose of the internal components:

**SMT-LIB Interpreter** (implemented in SMTLIBInterpreter.cpp) reads the input file in the smt-lib format [3], which is the standard input format for smt solvers. The interpreter executes all the commands from the file. In particular, it maintains the assertion stack and the options set by the user, calls solver when check-sat command is issued, and queries Solver if the user requires the model with the command get-model.

ing and underapproximating bdds. Precision of approximations depends on parameters set by the solver component.

**Cache** (implemented as a part of ExprToBDDTransformer.cpp) maintains for each converted subformula and subterm the corresponding bdd or a vector of bdds, respectively. Each of the three solvers has its own cache. When an approximating solver increases precision of the approximation, entries of its cache that can be affected by the precision change are invalidated. All the caches are internally implemented by hash-tables.

#### **3 Implementation**

Q3B is implemented in C++17, is open-source and available under MIT license on GitHub: https://github.com/martinjonas/Q3B. The project development process includes continuous integration and automatic regression tests.

Q3B relies on several external libraries and tools. For representation and manipulation with bdds, Q3B uses the open-source library cudd 3.0 [23]. Since cudd does not support bit-vector operations, we use the library by Peter Navr´atil [19] that implements bit-vector operations on top of cudd. The algorithms in this library are inspired by the ones in the bdd library BuDDy1 and they provide a decent performance. Nevertheless, we have further improved its performance by several modifications. In particular, we added a specific code for handling expensive operations like bit-vector multiplication and division when arguments contain constant bdds. This for example considerably speeds up multiplication whenever one argument contains many constant zero bits, which is a frequent case when we use the variable bit-width approximation fixing some bits to zero. Further, we have fixed few incorrectly implemented bit-vector operations in the original library. Finally, we have extended the library with the support for do-not-know bits in inputs of the bit-vector operations and we have implemented abstract versions of arithmetic operations that can produce do-not-know bits when the result exceeds a given number of bdd nodes.

For parsing the input formulas in smt-lib format, Q3B uses antlr parser generated from the grammar2 for smt-lib 2.6 [2]. We have modified the grammar to correctly handle bit-vector numerals and to support push and pop commands without numerical argument. The parser allows Q3B to support all bitvector operations and almost all smt-lib commands except get-assertions, get-assignment, get-proof, get-unsat-assumptions, get-unsat-core, and all the commands that work with algebraic data-types. This is in sharp contrast with the previous experimental versions of Q3B, which only collected all the assertions from the input file and performed the satisfiability check regardless of the rest of the commands and of the presence of the check-sat command. The reason for this was that the older versions parsed the input file using the Z3 C++ api, which can provide only the list of assertions, not the rest of the smt-lib script. Thanks to the new parser, Q3B 1.0 can also provide the user

1 https://sourceforge.net/projects/buddy/.

2 https://github.com/julianthome/smtlibv2-grammar.

with a model of a satisfiable formula after calling get-model; this important aspect of other smt solvers was completely missing in the previous versions.

On the other hand, C++ api of the solver Z3 is still used for internal representation of parsed formulas. The Z3 C++ api is also used to perform manipulations with formulas, such as substitution of values for variables, and some of the formula simplifications. Note that these are the only uses of Z3 api in Q3B during solving the formula; no actual smt- or sat-solving capabilities of Z3 are used during the solving process.

Some classes of Q3B, in particular Solver, FormulaSimplifier, and UnconstrainedVariableSimplifier, expose a public C++ api that can be used by external tools for smt solving or just performing formula simplifications. For example, Solver exposes method Solve(formula, approximationType), which can be used to decide satisfiability by the precise solver, the underapproximating solver, or the overapproximating solver. Solver also exposes the method SolveParallel(formula), which simplifies the input formula and runs all three of these solvers in parallel and returns the first result as depicted in Fig. 1.

#### **4 Experimental Evaluation**

We have evaluated the performance of QB3 1.0 and compared it to the latest versions of smt solvers Boolector (v3.0), CVC4 (v1.6), and Z3 (v4.8.4). All tools were used with their default settings except for CVC4, where we used the same settings as in the paper that introduces quantified bit-vector solving in CVC4 [20], since they give better results than the default CVC4 settings. As the benchmark set, we have used all 5751 quantified bit-vector formulas from the smt-lib repository. The benchmarks are divided into 8 distinct families of formulas. We have executed each solver on each benchmark with cpu time limit 20 min and ram limit of 8 GiB. All the experiments were performed in a Ubuntu 16.04 virtual machine within a computer equipped with Intel(R) Core(TM) i7-8700 CPU @ 3.20 GHz cpu and 32 GiB of ram. For reliable benchmarking we employed BenchExec [4], a tool that allocates specified resources for a program execution and precisely measures their usage. All scripts used for running benchmarks and processing their results, together with detailed descriptions and some additional results not presented in the paper, are available online3.

Table 1 shows the numbers of benchmarks in each benchmark family solved by the individual solvers. Q3B is able to solve the most benchmarks in benchmark families *2017-Preiner-scholl-smt08*, *2017-Preiner-tptp*, *2017-Preiner-UltimateAutomizer*, *2018-Preiner-cav18*, and *wintersteiger*, and it is competitive in the remaining families. In total, Q3B also solves more formulas than each of the other solvers: 116 more than Boolector, 83 more than CVC4, and 139 more than Z3. Although the numbers of solved formulas for the solvers seem fairly similar, the cross-comparison in Table 2 shows that the differences among the individual solvers are actually larger. For each other solver, there are at least

3 https://github.com/martinjonas/q3b-artifact.

**Table 1.** For each solver and benchmark family, the table shows the number of benchmarks from the given family solved by the given solver. The column *Total* shows the total number of benchmarks in the given family. The last line provides the total cpu times for the benchmarks solved by all four solvers.

**Table 2.** For all pairs of the solvers, the table shows the number of benchmarks that were solved by the solver in the corresponding row, but not by the solver in the corresponding column. The column *Uniquely solved* shows the number of benchmarks that were solved only by the given solver.

143 benchmarks that can be solved by Q3B but not by the other solver. We think this shows the importance of developing an smt solver based on bdds and approximations besides the solvers based on quantifier instantiation.

#### **5 Conclusions and Future Work**

We have described the architecture and inner workings of the first stable version of the state-of-the-art smt solver Q3B. Experimental evaluation on all quantified bit-vector formulas from smt-lib repository shows that this solver slightly outperforms other state-of-the-art solvers for such formulas.

As future work, we would like to drop the dependency on the Z3 api: namely to implement our own representation of formulas and reimplement all the simplifications currently outsourced to Z3 api directly in Q3B. We also plan to extend some simplifications with an additional bookkeeping needed to construct a model of the original formula. With these extensions, all simplifications could be used even if the user wants to get a model of the formula. We would also like to implement production of unsatisfiable cores since they are also valuable for software verification.

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

## **CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis**

Andrew Reynolds1, Haniel Barbosa1,

Andres Notzli ¨ 2(B) , Clark Barrett2, and Cesare Tinelli1

1 The University of Iowa, Iowa City, USA 2 Stanford University, Stanford, USA<EMAIL_ADDRESS>
**Abstract.** We present CVC4SY, a syntax-guided synthesis (SyGuS) solver based on three bounded term enumeration strategies. The first encodes term enumeration as an extension of the quantifier-free theory of algebraic datatypes. The second is based on a highly optimized brute-force algorithm. The third combines elements of the others. Our implementation of the strategies within the satisfiability modulo theories (SMT) solver CVC4 and a heuristic to choose between them leads to significant improvements over state-of-the-art SyGuS solvers.

#### **1 Introduction**

Syntax-guided synthesis (SyGuS) [3] is a recent paradigm for program synthesis, successfully used for applications in formal verification and programming languages. Most SyGuS solvers perform counterexample-guided inductive synthesis (CEGIS) [16]: a refinement loop in which a learner proposes solutions, and a verifier, generally a satisfiability modulo theories (SMT) solver [8,9], checks them and provides counterexamples for failures. Generally, the learner enumerates some set of terms, while pruning spurious ones [17]. The simplicity and efficacy of enumerative SyGuS have made it the de facto approach for SyGuS, although alternatives exist for restricted fragments [4,14].

In previous work [14], we have shown how the SMT solver CVC4 [5] can itself act as an efficient synthesizer. This tool paper focuses on recent advances in the enumerative subsolver of CVC4, culminating in the current SyGuS solver CVC4SY. Figure 1 shows its main components. The term enumerator is parameterized by an enumeration strategy chosen before solving: CVC4SY S, whose constraint-based (smart) enumeration allows for numerous optimizations (Sect. 2); CVC4SY F, based on a new approach for (fast) enumerative synthesis (Sect. 3), which has significant advantages with respect to the enumerative solver CVC4SY S and other state-of-the-art approaches; and CVC4SY H, based on a hybrid approach combining smart and fast enumeration (Sect. 4). All strategies are fully integrated in CVC4, meaning they support inputs in many background theories, including arithmetic, bit-vectors, strings, and floating point. We evaluate these approaches on a large set of benchmarks (Sect. 5).

**Fig. 1.** Architecture of CVC4SY.

*The Problem.* A syntax-guided synthesis problem for a function f in a background theory T consists of a set of semantic restrictions, or specification, for f given by a (second-order) T-formula of the form Df.ϕ[f], and a set of syntactic restrictions on the solutions for f, typically expressed as a context-free grammar. An *enumerative* approach to this problem combines a *term enumerator* and a *solution verifier* for solving synthesis conjectures. The role of the term enumerator is to output a stream of terms t1, t2,... over some tuple x¯ of variables representing the inputs of f, where each ti[¯x] is a candidate solution. The role of the solution verifier is to check for each ti whether it is a solution for f by determining if the negated conjecture ϕ[λx.t ¯ i] is unsatisfiable.

*Bounded* term generation considers terms based on an ordering such as term size (the number of non-nullary symbols in a term). For each k = 0, 1, 2,..., the term enumerator outputs a *finite* set Sk of terms, each of size at most k. Bounded term generation in CVC4SY is *complete* in the sense that, for any k, if f has a solution of size at most k, then at least one of the terms in Sk is a solution for f. The effectiveness of an approach for (complete) bounded term generation can be evaluated based on two criteria: (i) the number of terms it generates and (ii) the rate at which it generates them.

We follow two approaches for enumerative SyGuS in CVC4SY, each optimized for one of the criteria above: a *smart* approach and a *fast* one. The first aims to generate reasonably quickly the smallest set of terms while maintaining completeness, while the second aims to generate terms as quickly as possible.

*Technical Preliminaries.* As we showed in previous work [14], syntactic restrictions can be conveniently represented as a set of *(algebraic) datatypes*, for which some SMT solvers have dedicated decision procedures [7,13]. For instance, given a function f : (x : Int) ˆ (y : Int) Ñ Int and the context-free grammar R below specifying what integer (I) and Boolean (B) terms can appear in candidate solutions for f:

$$I ::= 0 \mid 1 \mid x \mid y \mid I + I \mid I - I \mid \text{ite}(B, I, I) \tag{1}$$

$$B \implies B \gg B \quad | \ I \approx I \quad | \lnot B \mid B \land B \tag{2}$$

our SyGuS solver generates the following mutually recursive datatypes:

$$\mathcal{I} = \mathbf{0} \mid \mathbf{1} \mid \mathbf{x} \mid \mathbf{y} \mid \mathsf{plus}(\mathcal{I}, \mathcal{I}) \mid \mathsf{minus}(\mathcal{I}, \mathcal{I}) \mid \mathsf{ite}(\mathcal{B}, \mathcal{I}, \mathcal{I}) \tag{3}$$

$$\mathcal{B} = \mathsf{geq}(\mathcal{Z}, \mathcal{Z}) \; | \; \mathsf{eq}(\mathcal{Z}, \mathcal{Z}) \; | \; \mathsf{not}(\mathcal{B}) \; | \; \mathsf{and}(\mathcal{B}, \mathcal{B}) \tag{4}$$

Each datatype constructor corresponds to a production rule of R, e.g. plus corresponds to the rule I ::= I +I. A datatype term such as plus(x, y) represents the arithmetic term x + y. We will use these datatypes as a running example.

For a datatype term t, we write isC(t) to denote the *discriminator* predicate that is satisfied exactly when t is interpreted as a datatype whose top constructor is C. We write selτ n(t) to denote a *shared selector* [15] applied to t, interpreted as the n*th* child of t with type τ if one exists, and interpreted as an arbitrary element of τ otherwise. A term consisting of zero or more consecutive nested applications of shared selectors applied to a term t is a *shared selector chain (for* t*)*.

#### **2 Smart Enumerative SyGuS**

Our *smart enumerative SyGuS* approach CVC4SY S, is based on finding solutions for an evolving set of constraints in an extension of the quantifier-free fragment of algebraic datatypes. These constraints are constructed to rule out many redundant solutions while not overconstraining the problem, potentially missing actual solutions.

In detail, candidate solutions for the function f : τ1 → τ2 to be synthesized are constructed by maintaining a set of constraints F, initially empty, for a first-order variable d ranging over the datatype representing τ2. For example, consider again the function f with the syntactic restrictions expressed by the datatypes in Eqs. 3 and 4. If the term generator finds a model for F, it provides to the solution verifier the integer term which corresponds to the value of d in the model; for example, it provides x + 1 when d is interpreted as plus(x, 1). In turn, if the solution verifier finds that x+ 1 is not a solution, it provides the *blocking constraint* isplus(d) \_ isx(selI 1 (d)) \_ is1(selI 2 (d)), i.e., the datatype constraint that rules out the current value for d, which is then added to F. This is a *syntactic* constraint on future candidate solutions from the term generator. Its atoms are discriminators applied to shared selector chains.

CVC4SY S uses a number of optimization techniques in addition to the basic loop above, which we describe in the remainder of this section. These techniques produce blocking constraints via the lemmas-on-demand paradigm [6] that eagerly rule out spurious candidates, *prior* to the solution verification step. Additionally, whenever possible, it *strengthens* blocking constraints via novel generalization techniques, with the effect of ruling out larger classes of candidates.

*Blocking via Theory Rewriting with Structural Generalization.* As we describe in previous work [14], the enumerative solver of CVC4 uses its rewriter as an oracle for discovering when candidate solutions are redundant. The motivation is that for any two equivalent terms t and s, only one of them needs to be checked with the solution verifier, since either both t and s are solutions to the synthesis conjecture or neither is. Given a term t, we write tÓ to denote its *rewritten form*. Note that it is possible for equivalent terms not to have the same rewritten form. This is a consequence of the trade-offs in the implementation of CVC4's rewriter, which must balance efficiency and completeness.

As an example, suppose that the term enumerator previously generated x+y and that d's current value is the datatype term representing y + x, where, however, (x + y)Ó = (y + x)Ó. We first generate a blocking constraint template R[z] of the form isplus(z)\_ isy(selI 1 (z))\_isx(selI 2 (z)), where z is a fresh variable. This template is subsequently instantiated with z ÞÑ u for any shared selector chain u of type I that currently (or later) appears in F, starting with d itself. This has the effect of ruling out all candidate solutions that have y + x as a subterm, which is justified by the fact that each such term is equivalent to one in which all occurrences of y + x are replaced by x + y.

We employ a refinement of this technique, which we call *theory rewriting with structural generalization*, which searches for and then blocks only the minimal skeleton of the term under test that is sufficient for determining its rewritten form. For example, consider the if-then-else term t = ite(x « 0 ^ y ě 0, 0, x), This term is equivalent to x, regardless of the value of predicate y ě 0. This can be confirmed by the rewriter by computing that ite(x « 0 ^ w, 0, x)Ó = x where w is a fresh Boolean variable. Then, instead of generating a constraint that blocks only (the datatype value corresponding to) t, we generate a stronger constraint that does not depend on the subterm y ě 0. In other words, this blocking constraint rules out all candidate solutions that contain the subterm ite(x « 0^w, 0, x), for *any* term w. We compute these generalizations using a recursive algorithm that iteratively replaces *each* subterm of the current candidate with a fresh variable, and checks whether its rewritten form remains the same.

*Blocking via CEGIS with Structural Generalization.* Synthesis solvers based on CEGIS maintain a list of *refinement points* that witness the infeasibility of previous candidate solutions. That is, given a synthesis conjecture Df. ∀x. ϕ ¯ [f, x¯], the solver maintains a growing list p¯1,..., p¯n of values for x¯ that witness the infeasibility of previous candidates u1,...,un for f. Then, when a new candidate u is generated, we first check whether ϕ[u, p¯i] is false for some i ď n. When a candidate u fails to satisfy ϕ[u, p¯i], CVC4SY S further applies a form of generalization analogous to the structural generalization described above. We call this *CEGIS with structural generalization*, where the goal is to find the minimal skeleton of u that also fails to satisfy some refinement point.

For example, suppose f is the function to synthesize, ϕ includes the constraint f(x, y) ď x − 1, and p1 = (3, 3) is a refinement point. Then, the candidate term u[x, y] = ite(x ě 0, x, y + 1) will be discarded, because ite(3 ě 0, 3, 4) ę 2. Notice, however, that *any* candidate u = ite(x ě 0, x, w) is falsified by p1, regardless of what w is, since u [3, 3] ď 2 is equivalent to 3 ď 2. This indicates that we can block *all* ite candidate terms with condition x ě 0 and true branch x. We can express this constraint in CVC4SY S by dropping the disjuncts that relate to the false branch of the ite term. This form of blocking is particularly useful when synthesizing multiple functions (f1, ...,fn), since it is often the case that a candidate for a single fi is already sufficient to falsify the specification, regardless of what the candidates for the other functions are.

*Evaluation Unfolding.* This technique uses *evaluation functions* to encode the relationship between the datatype terms assigned to d and their analogs in the theory T. For example, the evaluation function for the datatype I defined in (3) is a function EI : I ˆIntˆInt ÞÑ Int defined axiomatically so that EI(d, m, n) denotes the result of evaluating d by interpreting any occurrences of x and y in d respectively as m and n and interpreting the other constructors as the corresponding arithmetic/Boolean operators, e.g. EI(minus(x, y), 5, 3) is interpreted as 2. When a refinement point c¯is generated, we add a constraint requiring that the evaluation of d at c¯must satisfy the specification. For example, for conjecture Df. ∀x. f(x + 1, x) ď 0, and refinement point x ÞÑ 1, we add the constraint EI(d, 2, 1) ď 0. Then, when a literal isC(t) is asserted for a term t of type I, we can add a constraint corresponding to the one-step unfolding of the evaluation of t. Specifically, when isite(d) is asserted, we generate the constraint

$$\mathsf{is}\_{\mathsf{ite}}(d) \Rightarrow \mathsf{E}\_{\mathcal{T}}(d,2,1) \approx \mathsf{ite}(\mathsf{E}\_{\mathcal{B}}(\mathsf{sel}\_{1}^{\mathcal{B}}(d),2,1), \mathsf{E}\_{\mathcal{T}}(\mathsf{sel}\_{1}^{\mathcal{T}}(d),2,1), \mathsf{E}\_{\mathcal{T}}(\mathsf{sel}\_{2}^{\mathcal{T}}(d),2,1))$$

indicating that the evaluation of d on point (2, 1) indeed behaves like an ite term when d has top symbol ite. Our implementation adds these constraints for all terms t whose top symbols correspond to ite or Boolean connectives. For terms t whose top symbol is any of the other operators, we add constraints corresponding to their total evaluation of t when the value of t is fully determined, for example, t « plus(x, y) ñ EI(t, 2, 1) « 3. Notice this constraint with t = d along with the refinement constraint EI(d, 2, 1) ď 0 suffices to show that d cannot be plus(x, y).

#### **3 Fast Enumerative SyGuS**

The techniques in the previous section prune the search space so that often, only a small subset of the entire possible set of terms is considered for a given term size bound. The main bottleneck, however, is managing the large number of blocking constraints generated. Moreover, the benefits of this approach are limited when the grammar or specification does not admit opportunities for generalization.

For this reason, we have also developed CVC4SY F, which, in the spirit of other SyGuS solvers (notably ESOLVER [17]), relies on a principled brute-force approach for term generation. In contrast to other solvers, however, which are built as layers on top of the core SMT reasoner, CVC4SY F is fully integrated as a subsolver of CVC4, so communication with other components has almost no overhead. This technique, *fast enumerative synthesis*, does not use constraint solving to generate new terms. As a result, the majority of optimizations from Sect. 2 are incompatible with it.

*Algorithm.* To generate terms up to a given size k, we maintain a set Sk τ of terms of type τ and size k for each datatype τ corresponding to a non-terminal symbol of our input grammar R. First, we compute for each such τ the set Cτ of its *constructor classes*, an equivalence relation over the constructors of τ that groups them by their type. For example, the constructor classes for I are {x, y, 0, 1}, {plus, minus} and {ite}. Then, we use the following procedure for generating all terms of size k for type τ :

FASTENUM(τ , k):

For all:

The recursive procedure FASTENUM(τ , k) populates the set Sk τ of all terms of type τ with size k. These sets are cached globally. We incorporate an optimization that only adds terms C(t1,...,tn) to Sk τ whose corresponding terms in the theory T are unique up to rewriting. This mimics the effect of blocking via theory rewriting as described in Sect. 2. For example, plus(y, x) is not added to S1 I if that set already contains plus(x, y), noting that (x + y)Ó = (y + x)Ó. By construction of Sk τ for k ě 1, this has the cascading effect of excluding all terms having y + x as a subterm.

We observe that theory rewriting with structural generalization cannot be easily incorporated into this scheme since it requires the use of a constraint solver, something that the above algorithm seeks to avoid.

#### **4 Hybrid Approach: Variable-Agnostic Enumerative SyGuS**

We follow a third approach, in solver CVC4SY H, that combines elements of the previous approaches. The idea is to use the (smart) approach from Sect. 2 to generate terms, but then generate *multiple* candidate solutions from each term using a fast subprocedure we call a *concretizer*. We implement an instance of this scheme, which we call *variable-agnostic* term generation, that produces only terms that are unique modulo alpha-equivalence. In our running example, when a term t such as x + 1 is produced, the concretizer produces all terms generated by the grammar R that are alphaequivalent to t, namely, {x + 1, y + 1} in this case. The advantage of this approach is that CVC4SY H can block any term whose variables are not canonically ordered; that is, assuming for instance that x ă y, it may block terms like 1 − y and y + y, noting they are alpha-equivalent to 1 − x and x + x, respectively. To implement this blocking scheme, we introduce unary Boolean predicates prex and postx for each variable x in our grammar, where prex (resp., postx) holds for t if and only if variable x occurs in a depth-first left-to-right traversal of our candidate term before (resp., after) traversing to the position indicated by the selector chain t. We encode the semantics of these predicates based on the arguments of constructors in our signature, e.g. isplus(z) ñ (prex(z) « prex(selI 1 (z)) ^ postx(selI 2 (z)) « postx(z)). We then assert that prex and prey are false for our top-level variable d, and require isy(z) ñ prex(z) for all z, stating that x must come before y in the traversal of any generated term.

This technique is useful for grammars with many variables, such as grammars in invariant synthesis problems, where the number of terms of small size is prohibitively large. Blocking based on theory rewriting (with generalization) from Sect. 2 is compatible with this technique and is used in CVC4SY H. However, the other optimizations are disabled, since they prune solutions in a way that is not agnostic to variables.

#### **5 Evaluation**

We evaluated the above techniques in CVC4SY on four benchmark sets: invariant synthesis benchmarks from the verification of Lustre [11] models; a set from work on synthesizing invertibility conditions for bit-vector operators [12] (IC-BV); a set of bit-vector invariant synthesis problems [2] (CegisT); and the SyGuS-COMP 2018 [1] benchmarks from five tracks: assorted problems (General), conditional linear arithmetic

**Table 1.** Summary of number of problems solved per benchmark set. Best results are in **bold**.

problems (CLIA), invariant synthesis problems (INV), and programming-by-examples problems [10] with a set over bit-vectors (PBE-BV) and another over strings (PBE-Str). We also considered separately the CrCi subset from General, which corresponds to cryptographic circuit synthesis. We ran our experiments on a cluster equipped with Intel E5-2637 v4 CPUs running Ubuntu 16.04, providing one core, 1800 s, and 8 GB RAM for each job. Results are summarized in Table 1 and Fig. 2. We denote the strategies from Sects. 2, 3, and 4 by **s**, **f** and **h**, respectively (smart, fast, and hybrid); disabling the optimizations from Sect. 2 is marked by "-" and the suffixes **r** (rewriting), **rg** (rewriting with structural generalization), **cg** (CEGIS with structural generalization), and **eu** (evaluation unfolding). We also evaluated two meta-strategies of CVC4SY: **a** and **a+si**. The auto strategy **a** picks a strategy based on the properties of the problem: **f** for PBE problems and for problems without the Boolean type or the ite operator in their grammar and **s** otherwise. Strategy **a+si** uses the single-invocation solver [14] on problems that are amenable to quantifier elimination and **a** otherwise. We use the state-of-the-art SyGuS solver EUSOLVER [4] (**EUS**) as a baseline, but only for SyGuS-COMP benchmarks due to limitations in its parser.

Overall, strategy **s** excels on more challenging benchmark sets such as Lustre and Gen-Crci, while strategy **f** excels on the majority of the others. The gains for **f** are especially significant on PBE problems, where it outperforms both **s** and **EUS** by several orders of magnitude. Such gains are significant given that CVC4 won this track at SyGuS-COMP 2018 by employing **s** alone, and a variant of **EUS** won it in 2017. This result can be explained as a consequence of two factors. First, the string and bitvector grammars contain many operators with the same type, making the constructor class optimization of the **f** algorithm very effective. Second, although not described in this paper, all solvers in our evaluation use divide-and-conquer algorithms for PBE problems [4], which are not compatible with the optimizations **cg** and **eu**. The most important optimization for all CVC4SY strategies and with all benchmark sets is **r**. The optimization **eu** is especially effective when grammars contain ite and Boolean connectives, such as those in the Lustre set and in some subsets of General, on which we can

**Fig. 2.** Cactus plot on commonly supported benchmark sets. The first scatter plot is for the Lustre set, the second for the Gen-Crci set, and the latter two for the 862 benchmarks from the PBE sets.

see the biggest gains of **s** with respect to **s-eu**; **cg** is more helpful for IC-BV, with a few harder benchmarks only solved due to this technique.

The first scatter plot in Fig. 2 shows the advantage of **h** over **s** on Lustre, a benchmark set containing invariant synthesis problems with dozens of variables. We remark this configuration excels at quickly finding small solutions for problems with many variables, although solves fewer problems overall. The second scatter plot shows that while **s** takes significantly longer on easy problems, it outperforms **f** in the long run. The last two plots show that **f** significantly outperforms the state of the art on PBE benchmarks.

For all benchmark sets, the auto strategy **a** chooses the best enumerative strategy of CVC4SY with only a few exceptions, and hence it is the default configuration of CVC4SY. Due to specialized synthesis techniques [4,14], both **a+si** and **EUS** outperform the purely enumerative strategies of CVC4. This is reflected in the cactus plot on the commonly supported benchmark sets, where **a** and **f** solve more benchmarks than **EUS** for lower times but then **EUS** solves more benchmarks in the end. For **a+si**, the cactus plot shows that it outperforms **EUS** significantly. Nevertheless, we remark that **a+si** is able to solve only 393 (16%) of the overall benchmarks using only single invocation techniques. Hence, we conclude that both smart and fast enumerative strategies are critical subcomponents in our approach to syntax-guided synthesis.

**Acknowledgments.** This work was partially supported by the National Science Foundation under award 1656926 and by the Defense Advanced Research Projects Agency under award FA8650-18-2-7854.

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

## **Incremental Determinization for Quantifier Elimination and Functional Synthesis**

Markus N. Rabe(B)

Google, Mountain View, CA, USA<EMAIL_ADDRESS>
**Abstract.** Quantifier elimination and its cousin functional synthesis are fundamental problems in automated reasoning that could be used in many applications of formal methods. But, effective algorithms are still elusive. In this paper, we suggest a simple modification to a QBF algorithm to adapt it for quantifier elimination and functional synthesis. We demonstrate that the approach significantly outperforms previous algorithms for functional synthesis.

#### **1 Introduction**

Given a Boolean formula ∃Y.ϕ with free variables X, *quantifier elimination* (also called *projection*) is the problem to find a formula ψ ≡ ∃Y.ϕ that only contains variables X. Closely related, the *functional synthesis* problem is to find a function fy : 2X → B for all y ∈ Y , such that ϕ[Y → fy(X)] ≡ ∃Y.ϕ.

Quantifier elimination and functional synthesis are fundamental operations in automated reasoning, computer-aided design, and verification. Hence, progress in algorithms for these problems benefits a broad range of applications of formal methods. For example, typical algorithms for reactive synthesis reduce to computing the safe region of a safety game through repeated quantifier eliminations [1–3] or directly employ functional synthesis [4]. Until today, algorithms for quantifier elimination often involve (reduced ordered) Binary Decision Diagrams (BDDs) [5]. However, BDDs often grow exponentially for applications in verification, and extracting formulas (or strategies, etc.) from BDDs typically results in huge expressions. The search for alternatives resulted in CEGAR-style algorithms [6–10].

In this work, we take look at the closely related field of QBF solving. There pure CEGAR solving [11–13] on the CNF representation is not competitive anymore [14], and it has been augmented by preprocessing [15,16], circuit representations [17–21], and Incremental Determinization (ID) [22]. It may hence be fruitful to leverage some of the recent developments of QBF.

The contribution of this work is a simple modification of ID to enable quantifier elimination and functional synthesis. Incremental Determinization (ID) is an algorithm for solving quantified Boolean formulas of the shape ∀X. ∃Y.ϕ, where

c The Author(s) 2019

M.N. Rabe–Work partially done at University of California at Berkeley.

I. Dillig and S. Tasiran (Eds.): CAV 2019, LNCS 11562, pp. 84–94, 2019. https://doi.org/10.1007/978-3-030-25543-5\_6

ϕ is a propositional formula in conjunctive normal form (CNF), i.e. 2QBF. It follows a proof-theoretic approach, very similar to a SAT solver, alternating between building a model (i.e. Skolem functions for the existential variables Y ) and a refutation proof [23]. This allows ID to provide a model (i.e. a Skolem function) when it determines that a formula is true, which sets it apart from other QBF algorithms.

The modification of ID to enable quantifier elimination for a given formula ∃Y.ϕ is very simple: We run ID on the formula as if it was a quantified Boolean formula ∀X. ∃Y.ϕ, where X are the free variables, but add ϕ to the conflict check within ID. This suppresses the UNSAT result in the ID algorithm and it is hence forced to terminate with a model (that is, a function), which is guaranteed to satisfy the functional synthesis requirements. Quantifier elimination is then only a substitution away.

Our experimental evaluation shows that ID significantly outperforms previous algorithms for functional synthesis and quantifier elimination.

This paper is structured as follows: We review related work in Sect. 2 and introduce standard notation in Sect. 3. In Sect. 4 we first review the Incremental Determinization algorithm before introducing the change necessary to lift it to functional synthesis. The experimental evaluation is in Sect. 5. We summarize the current state of the tool CADET in Sect. 6 and conclude the paper in Sect. 7.

#### **2 Related Work**

*Functional Synthesis.* Early works on functional synthesis tried to exploit Craig interpolation, but did not scale well enough [24]. This was followed by first attempts to use CEGAR [6], which failed, however, to surpass the performance of BDDs [7]. More recent works revisited the use of BDDs, e.g. the tools SSyft [25] and RSynth [26,27]. This motivated the search for alternatives to BDDs [8–10]. At their core, these new algorithms all rely on counter-example guided abstraction refinement (CEGAR) [28], but they apply it in clever, compositional ways. However, they still inherit the well-known weaknesses of CEGAR (as, for example, discussed in the QBF literature): For the simple formula ϕ = - i<n xi ↔ yi, where n = |X| = |Y | and xi ∈ X and yi ∈ Y , CEGAR needs to browse through 2n satisfying assignments just to recover that the function we were looking for is f(x) = x.

The Back-and-Forth algorithm explores stronger abstraction using MaxSAT solvers as a means to reduce the number of assignments that CEGAR needs to explore [8]. ParSyn attempts to combat the problem with parallel compute power and a compositional approach [9]. This compositional approach has later been refined using a wDNNF decomposition [10].

*QBF Certification.* Some solvers and preprocessors for QBF have the ability to not only provide a yes/no answer, but also produce a certificate (i.e. Skolem functions) for their result [13,22,29,30]. While most QBF approaches suffer heavy performance penalties when asked to provide a certificate, Incremental Determinization naturally computes Skolem functions that can be extracted easily from the final state [22].

#### **3 Preliminaries**

Boolean formulas over a finite set of variables x ∈ X with domain B = {**0**, **1**} are generated by the following grammar:

$$\varphi \coloneqq \mathbf{0} \mid \mathbf{1} \mid x \mid \neg \varphi \mid (\varphi) \mid \varphi \vee \varphi \mid \varphi \wedge \varphi$$

Other logical operations, such as implication, XOR, and equality, are considered syntactic sugar with the usual definitions.

An *assignment x* to a set of variables X is a function *x* : X → B that maps each variable x ∈ X to either **1** or **0**. We denote the space of assignments to some set of variables X with 2X.

Given formulas ϕ and ϕ , and a variable x, we denote the substitution of x by ϕ in ϕ as ϕ[x → ϕ ]. We lift substitutions to sets of variables ϕ[X → tx] when tx maps each x ∈ X to a formula ϕ .

A *literal* l is either a variable x ∈ X, or its negation ¬x. We use l to denote the literal that is the logical negation of l. A disjunction of literals (l1 ∨ ... ∨ ln) is called a *clause* and their conjunction (l1 ∧...∧ln) is called a *cube*. We denote the variable of a literal by *var* (l) and lift the notion to clauses *var* (l1∨···∨ln) = {*var* (l1),..., *var* (ln)}.

A formula is in *conjunctive normal form* (CNF), if it is a conjunction of clauses. Throughout this exposition, we assume that the input formula is given in CNF. (The output, however, can be a non-CNF formula.) It is trivial to lift the approach to general Boolean formulas: Given a Boolean formula ϕ over variables X, the Tseitin transformation provides us a formula ψ with ϕ ≡ ∃Z.ψ, where Z are fresh variables [31]. Note that eliminating a group of variables X ⊆ X in ϕ is then the same as eliminating X ∪ Z in ψ.

*Resolution* is a well-known proof rule that allows us to merge two clauses as follows. Given two clauses C1 ∨ v and C2 ∨ ¬v, we call C1 ⊗v C2 = C1 ∨ C2 their *resolvent* with pivot v. The resolution rule states that C1 ∨ v and C2 ∨ ¬v imply their resolvent. Resolution is *refutationally complete* for Boolean formulas in CNF, i.e. given a formula in CNF that is equivalent to false, we can derive the empty clause using only resolution.

#### **4 Lifting Incremental Determinization**

In the sequel, we formally define functional synthesis, review the working principle of Incremental Determinization for 2QBF, discuss how the solver state corresponds to functions, and then introduce the modification to Incremental Determinization to turn it into an algorithm for functional synthesis. The *functional synthesis* problem is to find a function fy : 2X → B for all y ∈ Y , such that ϕ[Y → fy(X)] ≡ ∃Y.ϕ. Functional synthesis is closely related to solving 2QBF: Given a true 2QBF problem ∀X. ∃Y.ϕ, any Skolem function that is a model for the formula is also a solution to the functional synthesis problem for variable sets X and Y . Only for false 2QBF there is a difference between the problems: if there is an assignment *x* to X for which there is no assignment to Y , the 2QBF cannot be proven with a Skolem function, but the functional synthesis problem still requires us to produce a function f. It is clear that for input *x* the f can produce any output. We will exploit this similarity between 2QBF and functional synthesis in the following to lift the Incremental Determinization algorithm to functional synthesis.

#### **4.1 Working Principle of Incremental Determinization for 2QBF**

ID was originally introduced as an algorithm for 2QBF, the fragment of quantified Boolean formulas with at most one quantifier alternation. Given a formula ∀X. ∃Y.ϕ, ID alternates between constructing a model (i.e. a Skolem function) to prove the formula correct, and constructing a Q-resolution proof to refute the formula [32]. During model construction, ID identifies which variables in Y have unique Skolem functions considering the current set of clauses. When all variables with unique Skolem functions are identified, ID greedily introduces additional clauses to reduce the space of possible Skolem functions, such that the remaining variables may get unique Skolem functions, too. Whenever the model construction ends up in a dead-end (=conflict), ID switches to constructing a refutation proof [32] and derives clauses using resolution. As soon as ID found a clause that prevents the model construction from trying the same partial model again, it switches back to the model search. Since there are only finitely many clauses and models, either the model construction or the refutation proof must eventually finish [22,23].

*Example 1.* We will use the following formula as a running example:

$$\begin{array}{c} \left( \forall x\_1, x\_2. \exists y\_1, y\_2. \, y\_3. \, (x\_1 \lor \neg y\_1) \land (\neg x\_1 \lor y\_1) \land \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \left( y\_1 \lor \neg y\_2 \right) \land \left( \neg y\_1 \lor \neg x\_2 \lor y\_2 \right) \land \\ \qquad \qquad \qquad \qquad \qquad \left( \neg y\_1 \lor y\_3 \right) \land \left( y\_2 \lor \neg y\_3 \right) \land \left( x\_2 \lor \neg y\_3 \right) \end{array} \right)$$

Looking at the first two clauses it is clear that y1 is uniquely determined by x1 and y1's Skolem function must be fy1 (X) = x1. For this step, we intentionally ignore all clauses of y1 that contain y2 and y3, as they do not yet have a Skolem function and we have to consider them as undefined. The other clauses containing y1 will only become relevant when looking for Skolem functions for y2 and y3.

Variables y2 and y3 do not have *unique* Skolem functions in the formula above. ID would now greedily add a *decision clause*, such as (x2 ∨ ¬y2), to also make the Skolem function for y2 unique. The added clause, plus clauses 3 and 4 in the formula define: fy2 (X) = fy1 (X) ∧ x2.

This results in the situation that there is no Skolem function for y3: For the assignment x1 → **1**, x2 → **0**, the functions for y1 and y2 assign y1 → **1**, y2 → **0**. Then clauses 4 and 5 cannot be satisfied both by y3, which means there is a conflict for this assignment to the universals. During conflict analysis, ID would now resolve clauses 5 and 6 to obtain clause (¬y1 ∨ y2), and then backtrack to the point before introducing the decision clause. -

#### **4.2 Representation of Functions**

What is particularly interesting about ID is its ability to produce Skolem functions when it has proven a formula correct. Other than previous QBF algorithms, these Skolem functions are produced without any overhead.

ID avoids costly representations of Skolem functions: It maintains a set D ⊆ Y of variables that have a unique Skolem function, and its state includes a formula δ characterizing the input-output behavior of the Skolem functions for variables D. Formula δ satisfies ∀X. ∃!D. δ, where ∃!D means that there exists exactly one assignment to D. We can thus think of δ also as a function fδ mapping X assignments to D assignments.

*Example 2.* Back to our running example. After identifying a unique Skolem function for y1, formula δ consists exactly of the first two clauses of the formula, (x1 ∨¬y1)∧(¬x1 ∨y1). After adding the decision clause and identifying a unique Skolem function for y2, δ consists exactly of the first four clauses and the decision clause. -

#### **4.3 Conflict Checks in ID**

The formulas representing functions have primarily one purpose: to check for the existence of *conflicts*. Whenever we attempt to grow the set D by a variable v, we need to check whether v has a unique Skolem function. This check consists of two parts; given an arbitrary universal assignment *x* ∈ 2X,

To formally define this, let us consider the clauses (d1 ∨···∨dn ∨l) in ϕ that contain a literal l of variable v and otherwise only contain literals di of variables in D and X. We call these the clauses with *unique consequence*, as they can be read as implications (¬d1 ∧ ··· ∧ ¬dn ⇒ l), and we call ¬d1 ∧ ··· ∧ ¬dn the antecedent of that clause. Further, we define Al as the disjunction over all antecedents of literal l. (Note that Al depends on D and therefore changes as the state of the solver progresses.)

The two checks from above can now be defined as follows:

Checking for case (1) can be efficiently approximated [22], but checking for case (2) cannot easily be avoided. We thus query a SAT solver with δ∧Av ∧A¬v to perform a conflict check.

*Example 3.* We revisit the conflict described in Example 1. The starting point is the situation when D = {y1, y2} and δ consists of the first four clauses of the formula as well as the decision clause (x2 ∨ ¬y2). The antecedents of y3 are Ay3 = y1 and A¬y3 = ¬y2∨¬x2. It is easy to verify that the universal assignment x1 → **1**, x2 → **0**, y1 → **1**, y2 → **0** satisfies the conflict criterion δ∧Av ∧A¬v. -

#### **4.4 Functional Synthesis**

Remember that in the case of functional synthesis for ϕ over sets of variables X and Y , we search for a function f : 2X → 2Y such that f produces a satisfying assignment whenever it can, but can produce anything when there is no assignment to Y satisfying the formula. In case there are satisfying assignments to Y for all X, we can simply run ID as if it was a QBF ∀X. ∃. ϕ to obtain a Skolem function that also satisfies the functional synthesis criterion. In the other case, that there is an X for which there is no assignment to Y satisfying ϕ, ID for 2QBF would eventually detect a conflict that did not depend on a decision and return with UNSAT.

In order to lift ID to functional synthesis, we want to ignore universal assignments that have no satisfying assignment to Y . A simple way to suppress these conflicts is to add ϕ to the conflict check. In order for an assignment to X to remain a conflict, we must now additionally find an assignment to Y that demonstrates that the conflict could be prevented by a different decision.

All other parts of ID, including the extraction of functions, remain untouched. In particular, termination is still guaranteed, as the greedy model construction either results in a function for all variables in Y or in a conflict, upon which at least one model is excluded through resolution.

*Example 4.* For the conflict in our running example, the universal assignment x1 → **1**, x2 → **0** is excluded in the modified conflict check. Consider the UNSAT core consisting of clauses 2, 5, and 7 for that universal assignment: propagate y1 → **1** using clause 2; propagate y3 → **1** using clause 5; and finally propagate y3 → **0** using clause 7. So, instead of going into conflict analysis and backtracking, ID for functional synthesis concludes that it has found a function for all existential variables and terminates.

#### **4.5 Quantifier Elimination**

Given a formula ∃Y.ϕ with free variables X, *quantifier elimination* is the problem to find a formula ψ ≡ ∃Y.ϕ over variables X only. Hence, given a solution f to the functional synthesis problem for ϕ, we only have to substitute Y by f in ϕ to obtain the projected formula.

#### **5 Experimental Evaluation**

We implemented the modifications to ID in CADET,1 a competitive 2QBF solver [22]. In this section, we compare CADET experimentally with existing

1 CADET is available at https://github.com/MarkusRabe/cadet.

**Fig. 1.** Log-scale cactus plot comparing the performance over all instances.

algorithms for functional synthesis. Additionally, we implemented a certificate checker for functional synthesis and for quantifier elimination, to make sure that the computed functions are correct. The certificate checker only shares the code for AIGER circuits and the SAT solver (of which we have tried several), but is completely independent otherwise to reduce the chance of correlated bugs. The results of CADET have been checked with the proof checker; running times reported below are excluding the time to check the certificates.

So far, there is no standard benchmark for functional synthesis or quantifier elimination. Like previous works on functional synthesis, we resort to using the 2QBF benchmark from QBFEVAL'17 [14], and re-interpret them as functional synthesis problems. The 2QBF benchmark from QBFEVAL'17 is a collection of 384 formulas from various domains, mostly from software verification, program synthesis, and logical equivalences [33–36].

We compare CADET to the most recent tools on functional synthesis, BaF-Syn [8] and BFSS [10], the latter of which has been shown to consistently outperform the earlier, BDD-based tools SSyft [25] and RSynth [26,27]. We ran CADET in two configurations: with (CADET+) and without (CADET) its CEGAR module [23]. We present the results as a cactus plot, which is obtained by running each tool on all formulas, sorting the running times for each tool separately. A point x, y in this plot means that x formulas were solved in less than time y. Note that the time axis is in log-scale (Fig. 1).

CADET shows a clear edge in performance: it is one to two orders of magnitude faster than its strongest competitor, BFSS, and can solve significantly more formulas. But despite the clear performance advantage in this aggregate view, BaFSyn and BFSS can be faster for individual formulas or subfamilies of QBFEval, as shown in previous works [8,10].

#### **6 The Current State of CADET**

Originally designed as an experimentation platform, CADET has grown to become a performant and versatile tool for the synthesis of Boolean functions. It consistently wins awards at the annual QBFEVAL competitions, and is the only such tool able to prove all its results [14].

CADET reads specifications in the QDIMACS and the QAIGER formats, and now supports the synthesis of Boolean functions for 2QBF, functional synthesis, and quantifier elimination with the command line options -c [file], -f [file], and -e [file]. The functions computed by CADET are much smaller compared to those found by CEGAR-based algorithms [22], and in its default configuration, CADET double-checks its results before reporting them. This can be deactivated by the flag --dontverify.

It has also been integrated in py-aiger [37], a Python package for the convenient handling of circuits due to Marcell Vazquez-Chanlatte, which enables us to easily model and prototype new approaches. For example, we can write:

```
import aiger analy si s as aa
import aigerbv as bv
x = bv . atom (32 , ' x ' ) # Create a 32 b i t var iable
y = bv . atom (32 , ' y ' )
expr = (x != y)
result = aa . eliminate ( expr , [ 'y ' ] )
assert aa . is equal (x, result )
```
CADET also has an experimental reinforcement learning interface that allows us to automatically learn decision heuristics with the help of graph neural networks. A recent effort shows that there is huge potential in learning better branching heuristics from scratch [38].

#### **7 Conclusions**

In this work, we extended ID with the ability to solve functional synthesis and quantifier elimination problems. The extension is very simple—we only need to add the clauses of the original formula to its conflict check. The resulting algorithm significantly outperforms previous algorithms for functional synthesis.

**Acknowledgements.** The author wants to thank to Shubham Goel, Shetal Shah, and Lucas Tabajara for insightful discussions and for their assistance with running their functional synthesis tools. In particular, I want to express my gratitude to Supratik Chakraborty for inspiring me to work on the topic in a discussion in the summer of 2016.

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

## Numerical Programs

## **Loop Summarization with Rational Vector Addition Systems**

Jake Silverman(B) and Zachary Kincaid

Princeton University, Princeton, USA<EMAIL_ADDRESS>
**Abstract.** This paper presents a technique for computing numerical loop summaries. The method synthesizes a rational vector addition system with resets (Q-VASR) that simulates the action of an input loop, and then uses the reachability relation of that Q-VASR to over-approximate the behavior of the loop. The key technical problem solved in this paper is to automatically synthesize a Q-VASR that is a *best abstraction* of a given loop in the sense that (1) it simulates the loop and (2) it is simulated by any other Q-VASR that simulates the loop. Since our loop summarization scheme is based on computing the *exact* reachability relation of a *best* abstraction of a loop, we can make theoretical guarantees about its behavior. Moreover, we show experimentally that the technique is precise and performant in practice.

#### **1 Introduction**

Modern software verification techniques employ a number of heuristics for reasoning about loops. While these heuristics are often effective, they are unpredictable. For example, an abstract interpreter may fail to find the most precise invariant expressible in the language of its abstract domain due to imprecise widening, or a software-model checker might fail to terminate because it generates interpolants that are insufficiently general. This paper presents a loop summarization technique that is capable of generating loop invariants in an expressive and decidable language and provides theoretical guarantees about invariant quality.

The key idea behind our technique is to leverage reachability results of vector addition systems (VAS) for invariant generation. Vector addition systems are a class of infinite-state transition systems with decidable reachability, classically used as a model of parallel systems [12]. We consider a variation of VAS, *rational VAS with resets (* Q-VASR*)*, wherein there is a finite number of rational-typed variables and a finite set of transitions that simultaneously update each variable in the system by either adding a constant value or (re)setting the variable to a constant value. Our interest in Q-VASRs stems from the fact that there is (polytime) procedure to compute a linear arithmetic formula that represents a Q-VASR's reachability relation [8].

Since the reachability relation of a Q-VASR is computable, the dynamics of Q-VASR can be analyzed without relying on heuristic techniques. However, there is a gap between Q-VASR and the loops that we are interested in summarizing. The latter typically use a rich set of operations (memory manipulation, conditionals, non-constant increments, non-linear arithmetic, etc) and cannot be analyzed precisely. We bridge the gap with a procedure that, for any loop, synthesizes a Q-VASR that simulates it. The reachability relation of the Q-VASR can then be used to over-approximate the behavior of the loop. Moreover, we prove that if a loop is expressed in linear rational arithmetic (LRA), then our procedure synthesizes a *best* Q-VASR abstraction, in the sense that it simulates any other Q-VASR that simulates the loop. That is, imprecision in the analysis is due to inherent limitations of the Q-VASR model, rather heuristic algorithmic choices.

One limitation of the model is that Q-VASRs over-approximate multi-path loops by treating the choice between paths as non-deterministic. We show that Q-VASRS, Q-VASR extended with control states, can be used to improve our invariant generation scheme by encoding control flow information and interpath control dependencies that are lost in the Q-VASR abstraction. We give an algorithm for synthesizing a Q-VASRS abstraction of a given loop, which (like our Q-VASR abstraction algorithm) synthesizes *best* abstractions under certain assumptions.

Finally, we note that our analysis techniques extend to complex control structures (such as nested loops) by employing summarization compositionally (i.e., "bottom-up"). For example, our analysis summarizes a nested loop by first summarizing its inner loops, and then uses the summaries to analyze the outer loop. As a result of compositionality, our analysis can be applied to partial programs, is easy to parallelize, and has the potential to scale to large code bases.

The main contributions of the paper are as follows:

#### **1.1 Outline**

This section illustrates the high-level structure of our invariant generation scheme. The goal is to compute a *transition formula* that summarizes the behavior of a given program. A transition formula is a formula over a set of program variables Var along with primed copies Var , representing the state of the program

```
procedure enqueue(elt):
  back := cons(elt,back)
  size := size + 1
procedure dequeue():
  if (front == nil) then
    // Reverse back, append to front
    while (back != nil) do
      front := cons(head(back),front)
      back := tail(back)
  result := head(front)
  front := tail(front)
  size := size - 1
  return result
           (a) Persistent queue
                                          procedure enqueue():
                                            back len := back len + 1
                                            mem ops := mem ops + 1
                                            size := size + 1
                                          procedure dequeue():
                                            if (front len == 0) then
                                              while (back len != 0) do
                                                 front len := front len + 1
                                                 back len := back len - 1
                                                 mem ops := mem ops + 3
                                            size := size - 1
                                            front len := front len - 1
                                            mem ops := mem ops + 2
                                          procedure harness():
                                            nb ops := 0
                                            while nondet() do
                                              nb ops := nb ops + 1
                                              if (size > 0 && nondet())
                                                 enqueue()
                                              else
                                                 dequeue()
                                                  (b) Integer model & harness
```
**Fig. 1.** A persistent queue and integer model. back len and front len models the lengths of the lists front and back; mem ops counts the number of memory operations in the computation.

before and after executing a computation (respectively). For any given program P, a transition formula **TF**-P can be computed by recursion on syntax:1

$$\begin{array}{c} \mathtt{TF}[\mathtt{x} := e] \triangleq \mathtt{x}' = e \land \bigwedge\_{\mathtt{y} \neq \mathtt{x} \in \mathtt{Var}} \mathtt{y}' = \mathtt{y} \\\\ \mathtt{TF}[\mathtt{if} \ c \ \mathtt{then} \ P\_{1} \ \mathtt{else} \ P\_{2}] \stackrel{\scriptstyle \triangleq}{=} \left( c \land \mathtt{TF}[P\_{1}] \right) \vee \left( \neg c \land \mathtt{TF}[P\_{2}] \right) \\\\ \mathtt{TF}[P\_{1}; P\_{2}] \stackrel{\scriptstyle \triangleq}{=} \exists X \in \mathtt{Z}. \mathtt{TF}[P\_{1}][\mathtt{Var}' \mapsto X] \land \mathtt{TF}[P\_{2}][\mathtt{Var} \mapsto X] \\\\ \mathtt{TF}[\mathtt{while} \ c \ \mathtt{do} \ P] \stackrel{\scriptstyle \triangleq}{=} \left( c \land \mathtt{TF}[P] \right) \stackrel{\scriptstyle \triangleq}{\land} \land \left( \neg c[\mathtt{Var} \mapsto \mathtt{Var}'] \right) \end{array}$$

where (−) is a function that computes an over-approximation of the transitive closure of a transition formula. The contribution of this paper is a method for computing this (−) operation, which is based on first over-approximating the input transition formula by a Q-VASR, and then computing the (exact) reachability relation of the Q-VASR.

1 This style of analysis can be extended from a simple block-structured language to one with control flow and recursive procedures using the framework of algebraic program analysis [13,23].

We illustrate the analysis on an integer model of a persistent queue data structure, pictured in Fig. 1. The example consists of two operations (enqueue and dequeue), as well as a test harness (harness) that non-deterministically executes enqueue and dequeue operations. The queue achieves O(1) amortized memory operations (mem ops) in enqueue and queue by implementing the queue as two lists, front and back (whose lengths are modeled as front len and back len, respectively): the sequence of elements in the queue is the front list followed by the reverse of the back list. We will show that the queue functions use O(1) amortized memory operations by finding a summary for harness that implies a linear bound on mem ops (the number of memory operations in the computation) in terms of nb ops (the total number of enqueue/dequeue operations executed in some sequence of operations).

We analyze the queue compositionally, in "bottom-up" fashion (i.e., starting from deeply-nested code and working our way back up to a summary for harness). There are two loops of interest, one in dequeue and one in harness. Since the dequeue loop is nested inside the harness loop, dequeue is analyzed first. We start by computing a transition formula that represents one execution of the body of the dequeue loop:

$$\mathbf{b} \mathbf{b} \mathbf{y\_{\mathsf{dq}}} = \mathbf{b} \mathbf{c} \mathbf{k} \mathbf{1} \mathbf{n} > 0 \land \begin{pmatrix} \mathbf{f} \mathbf{n} \mathbf{t} \texttt{.1en}' = \mathbf{f} \texttt{n} \texttt{.1en} + 1 \\ \wedge \texttt{back\\_len'} = \mathbf{back\\_len} - 1 \\ \wedge \texttt{mem\\_ops'} = \texttt{mem\\_ops} + 3 \\ \wedge \texttt{size'} = \texttt{size} \end{pmatrix}$$

Observe that each variable in the loop is incremented by a constant value. As a result, the loop update can be captured faithfully by a vector addition system. In particular, we see that this loop body formula is simulated by the Q-VASR Vdeq (below), where the correspondence between the state-space of *Body*deq and Vdeq is given by the identity transformation (i.e., each dimension of Vdeq simply represents one of the variables of *Body*deq).

$$
\begin{bmatrix} w \\ x \\ y \\ z \end{bmatrix} = \begin{bmatrix} 1 \ 0 \ 0 \ 0 \\ 0 \ 1 \ 0 \ 0 \\ 0 \ 0 \ 1 \ 0 \\ 0 \ 0 \ 0 \ 1 \end{bmatrix} \begin{bmatrix} \mathbf{f} \mathbf{n} \ \mathbf{n} \ \mathbf{l} \ \mathbf{n} \\ \mathbf{b} \ \mathbf{a} \mathbf{k} \ \mathbf{l} \ \mathbf{n} \\ \mathbf{m} \mathbf{m} \ \mathbf{o} \ \mathbf{s} \\ \mathbf{s} \ \mathbf{i} \mathbf{z} \end{bmatrix}; \quad V\_{\mathbf{d} \mathbf{a} \mathbf{q}} = \left\{ \begin{bmatrix} w \\ x \\ y \\ z \end{bmatrix} \to \begin{bmatrix} w+1 \\ x-1 \\ y+3 \\ z \end{bmatrix} \right\} \dots
$$

A formula representing the reachability relation of a vector addition system can be computed in polytime. For the case of Vdeq, a formula representing k steps of the Q-VASR is simply

$$w' = w + k \wedge x' = x - k \wedge y' = y + 3k \wedge z' = z. \tag{\dagger}$$