Powerful Techniques for the Automatic Generation of Invariants

Saddek Bensalem^{1}^{⋆}, Yassine Lakhnech^{2} ^{⋆⋆}, and Hassen Saidi ^{1}^{⋆⋆⋆}

1 VERIMAG, Miniparc-Zirst, Rue Lavoisier 38330 Montbonnot St-Martin, France. 2 Institut für Informatik und Praktische Mathematik Christian-Albrechts-Universität

zu Kiel, Preußerstr. 1-9, D-24105 Kiel, Germany.

Abstract. When proving invariance properties of programs one is faced with two problems. The first problem is related to the necessity of proving tautologies of the considered assertion language, whereas the second manifests in the need of finding sufficiently strong invariants. This paper focuses on the second problem and describes techniques for the automatic generation of invariants. The first set of these techniques is applicable on sequential transition systems and allows to derive so-called local invariants, i.e. predicates which are invariant at some control location. The second is applicable on networks of transition systems and allows to combine local invariants of the sequential components to obtain local invariants of the global systems. Furthermore, a refined strengthening technique is presented that allows to avoid the problem of size-increase of the considered predicates which is the main drawback of the usual strengthening technique. The proposed techniques are illustrated by examples.

1 Introduction

Model checking [17, 4, 13, 20] is by now a well-known method for proving properties of reactive programs. The main reason for its success is that it works fully automatically, i.e. without any intervention of the user. The price to pay for this feature is that it can only be applied on finite-state, or restricted classes of infinite state, programs.

On the other hand, there exist deductive methods to prove safety properties of reactive programs. These methods are based on a proof rule which can be formulated as follows. To prove that some given predicate P is an invariant of a given program S, i.e. that every reachable state of S satisfies P, it is necessary and sufficient to find a predicate Q with the following properties: 1.) Q is stronger than P, 2.) Q is preserved by every transition of S, i.e. for every states s and s′, if s satisfies Q and s′ is reachable from s by a transition, then also s′ satisfies Q, and 3.) Q is satisfied by every initial state of S. The predicate Q is called auxiliary predicate.

⋆ Bensalem@imag.fr, Currently visiting the Computer Science Laboratory, SRI

International ⋆⋆ yl@informatik.uni-kiel.de ⋆⋆⋆ Saidi@imag.fr

Although, this rule is sound and (relatively) complete, it provides only a partial answer to the verification problem of safety properties. For it leaves open (i) how to find the auxiliary predicate Q and (ii) how to prove that Q is preserved by every transition of S and satisfied by the initial states. Problem (ii) is related to the problem of proving tautologies of the underlying assertion language.

In this work, we describe techniques for automatically generating auxiliary predicates. We present the following strategies:

– Generalized reaffirmed invariance: This applies to transitions for which the value of the guard and of the expressions occurring on the right hand side of its assignment are not changed by the transition itself, i.e. they have the same value before and after the transition. This is more general than the one called reaffirmed invariants in [15, 14].

– Propagation of invariants: This technique allows to propagate an assertion that holds whenever control is at some fixed control location to other control locations. We consider two instances of this technique. The most general one allows to propagate even in the presence of loops. Again our technique is applicable in cases not covered by the propagation techniques presented in e.g. [15, 14].

– Refined strengthening: One of the most used techniques for strengthening invariants is by calculating the weakest (liberal) precondition [6] w.r.t. the considered invariant and taking it as a conjunct. A drawback of this method is that it increases the complexity of the considered predicate, and hence, after few steps its application leads in many cases to unmanageable predicates. We present a refined version of this method that allows to attenuate the blow up caused by applying this useful strengthening method.

– Combining Invariants: This method allows to combine invariants developed separately for the components of a given network S_{1} ∥ ⋯ ∥ S_{n} of transition systems to an invariant of the global system.

All predicates that can be generated by these strategies are proved to be invariant by construction. The use of these techniques for various mutual exclusion algorithms shows that they are promising. For instance, in case of the Bakery algorithm [12, 15], which is an infinite-state program, we generate an invariant that is sufficiently strong to prove the required property.

It is also important to note that these techniques are local in the sense that, in order to apply them, they do not require the full transition system to satisfy some restrictions, but rather subsets of control locations and variables are required to satisfy some condition.

The problem of automatically constructing invariants from program description has been intensively investigated in the seventieth leading to results reported in e.g. [11, 9, 3, 7]^{3}. Here, we present results which are to our knowledge new or extensions of existing ones. Other interesting recent results are reported in [2].

These techniques represent an important component of a tool which is being developed to support the computer-aided verification of safety properties of

3 This list of references is far from being exhaustive. See [15] for other references.

reactive programs. Here, we give a brief description of this tool (See [10] for a detailed discussion). It consists of the following components:

– Front-end: The front-end takes as input a description of a transition system written as a program in a simple programming language and a predicate to be proved as invariant of the described transition system. Then, it produces a PVS-theory [16] that mainly contains the verification conditions to be proved. The front-end analyses also the program and generates a file containing information needed to decide, for each control location, whether some invariant generation procedure can be applied.

– Automatic Invariant Generation: This is a module that contains procedures implementing several invariant generation techniques. In this paper, we present some of these techniques.

– Proof Manager: The user can try to prove that P is an invariant fully automatically. In this case, the system tries to prove that P is inductive, that is, P is preserved by each transition of the program. In case of success, this is reported to the user. Otherwise, the system tries to prove the invariance of P using predicates which are obtained by calling some invariant generating procedures. These predicates are guaranteed to be invariant by construction. In case the system is unable to prove the invariance of P, it may either do some strengthening or enter the interactive modus and requires the user’s guidance. This choice is made by the user.

– PVS is the theorem prover developed at SRI [16]. It is used during the automatic- as well as interactive proof procedure to discharge the verification conditions.

2 Transition Systems and Invariance Properties

We assume an underlying assertion language A that includes first-order predicate logic and interpreted symbols for expressing the standard operations and relations over some concrete domains. We assume to have the set of integers among these domains. Assertions (we also say predicates) in A are interpreted in states that assign values to the variables of A. Let Σ denote the set of states. Given a state s and a predicate P, we use the notation s ⊧ P to denote that s satisfies P, and use [[P]] to denote the set of states that satisfy P. Henceforth, we identify P and its characteristic set [[P]].

Definition 1. A transition system is a structure S = ⟨X, pc : DC, T, Init⟩, where

– X is a finite set {x_{1} : D_{1}, …, x_{n} : D_{n}} of typed data variables. Each variable x_{i} ranges over data domain D_{i}. We assume that the variables in X form a subset of those in A.

– pc is a control variable (or program instruction counter). It ranges over the finite domain DC. We assume that pc ∉ X.

– T is a finite set of transitions. A transition t is characterized by a quadruple (pc = d, g(Y), Z′ = e(U), pc′ = d′)^{4}, where Y, Z, U ⊆ X. The variables in

4 Z′ can be empty; this is the case when no variable is affected

Z are called the variables affected by transition t, and we denote by sour(t) (resp. tar(t)) the value d (resp. d′). These definitions are easily generalized to sets of transitions. Given a transition t = (pc = d, g(Y), Z′ = e(U), pc′ = d′), and states s and s′, s′ is called t-successor of s, denoted by s →_{t} s′, if the following conditions are satisfied: 1.) s satisfies the enabledness condition pc = d ∧ g(Y) of transition t and 2.) s′ satisfies s′(z_{i}) = e_{i}(s(U)), for each z_{i} ∈ Z, s′(x) = s(x), for each x with x ∉ Z, and s′(pc) = d′.

– Init is of the form I(X) ∧ pc = d_{0}. The conjunct I(X) specifies the initial condition on data variables, whereas pc = d_{0} specifies the initial value of the control variable. We call I the initial predicate of S and d_{0} its initial control location.

A transition system generates a set of sequences of states. Since we are only interested in invariance properties, we only consider finite sequences. A finite sequence σ = s_{0}, ⋯, s_{n} of states is called computation of S, if s_{0} satisfies Init and, for every i ∈ {0, …, n − 1}, there exists a transition t in T with s_{i} →_{t} s_{i+1}.

To define the semantics of the parallel construct, we define the product of two transition systems. Let S_{i} = ⟨X_{i}, pc_{i} : DC_{i}, T_{i}, Init_{i}⟩, for i = 1, 2, be transition systems. The product of S_{1} and S_{2}, denoted S_{1} ⨂ S_{2}, is a transition system ⟨X, pc : DC, T, Init⟩, where

– X = X_{1} ∪ X_{2} is the set of program variables.

– pc ranges over DC = DC_{1} × DC_{2}.

– A transition (pc = (d_{1}, d_{2}), g(Y), Z′ = e(U), pc = (d′_{1}, d′_{2})) is in T iff either • (pc_{1} = d_{1}, g(Y), Z′ = e(U), pc′_{1} = d′_{1}) ∈ T_{1} and d′_{2} = d_{2} or

• (pc_{2} = d_{2}, g(Y), Z′ = e(U), pc′_{2} = d′_{2}) ∈ T_{2} and d′_{1} = d_{1}.

– Init = I_{1} ∧ I_{2} ∧ pc = (d_{1,0}, d_{2,0}), where Init_{i} = I_{i} ∧ pc_{i} = d_{i,0}, for i = 1, 2.

Then, the set of computations of S_{1} ∥ S_{2} is defined to be that of S_{1} ⨂ S_{2}. Invariance Properties We consider a class of properties, named invariance properties (cf. [15]). Intuitively, a property P is an invariant of a transition system S, if in each state of the system S this property holds. In other words, each state that is reached during a computation of S satisfies P.

Definition 2. A state s is called reachable (accessible) in the transition system S, if there exists a computation s_{0}, ⋯, s_{n} of S such that s_{n} = s. We denote the set of reachable states by Reach(S). A predicate P is called invariance property of S (or invariant of S) iff Reach(S) ⊆ [[P]]. For d ∈ DC, we say that P is an invariant of S at d, if P ∨ ¬(pc = d) is an invariant of S.

Next, we briefly recall the basic idea for proving invariance properties of programs. This idea underlies many proof rules formulated in different settings (e.g. [8, 1, 15]). To do so, we recall the definition of some predicate transformers.

Definition 3. Given ρ ⊆ Σ × Σ, the predicate transformers pre[ρ], p̃re[ρ], and post[ρ] are defined by pre[ρ](P) = {s ∈ Σ | ∃s′ ∈ P · (s, s′) ∈ ρ}, p̃re[ρ](P) = ¬pre[ρ](¬P), and post[ρ](P) = {s′ ∈ Σ | ∃s ∈ P · (s, s′) ∈ ρ} Thus, pre[ρ](P) is the set of predecessors of P by ρ, post[ρ](P) is the set of successors of P, and p̃re[ρ](P) is the set of states which either do not have successors by ρ or all their successors are in P. Note that the p̃re[ρ] and post[ρ] are the weakest liberal precondition and strongest postcondition predicate transformers [6].

The main principle used in the literature for proving that a predicate P is an invariant of a system S, consists on finding an auxiliary predicate Q such that 1.) Q is stronger than P, 2.) every initial state satisfies Q, and 3.) Q is inductive, i.e. for all transitions t ∈ T, we have [[Q]] ⊆ p̃re[→_{t}](Q), or equivalently, post[→_{t} ](Q) ⊆ [[Q]].

This proof rule is unsatisfactory because it does not tell us how to find the auxiliary predicate Q. Finding Q is often the hard part in the proof of invariance properties.

In the next section, we present a set of techniques that, given a transition system S and a predicate P, automatically generate an auxiliary predicate that is by construction an invariant. In some cases, the generated predicate is strong enough to prove that P is an invariant.

3 Automatic Generation of Auxiliary Predicates

In this section we present some of the strategies for deriving auxiliary predicates we implemented in our tool. We concentrate on strategies which are to our knowledge new or extensions of strategies presented in other works (e.g. [9, 11, 15, 14, 2]). The auxiliary predicates derived using our strategies are proved to be invariant by construction. Generalized Reaffirmed Invariance without Cycles We begin with a strategy that can be applied to a control location d to derive an invariant under the assumption that all transitions that lead to d satisfy some restrictions we define below. This is a generalization of the reaffirmed invariance strategy presented in [15, 14].

Let S = ⟨X, pc : DC, T, I∧pc = d_{0}⟩ be given. For α ⊆ DC, let L(α) denote the set of transitions t with tar(t) ∈ α. Thus, L(α) is the set of transitions changing the value of the control variable to a value in α. We write L(d) instead of L({d}).

Consider a transition t = (pc = d_{1}, g(Y), Z′ = e(U), pc′ = d), with Z∩U = ∅. Then, for every states s and s′, if s →_{t} s′, then s′(Z) = e(s′(U)) and s′(U) = s(U). This suggests to take the predicate Z = e as invariant at d.

To formulate the general case, given a transition t as above, we denote by aff(t) the predicate Z = e(U) and by gu(t), the guard g(Y). Let, for d ∈ DC, Ass_{S}(d) = ⋁_{t∈L(d)}(gu(t) ∧ aff(t)), if d ≠ d_{0}; and I ∨ ⋁_{t∈L(d)}(gu(t) ∧ aff(t)), if d = d_{0},

where I is the initial predicate of S and d_{0} its initial control location.

Lemma 4. Let S be a given transition system with Init = I ∧ pc = d_{0} and let D ⊆ DC be such that for each d ∈ D and transition (pc = d_{1}, g(Y), Z′ = e(U), pc′ = d) in L(d) we have Z ∩ (Y ∪ U) = ∅. Then, for each d ∈ D, the predicate Ass_{S}(d) is an invariant of S at d.

We can actually formulate a strategy that generalizes the one above by relaxing the condition Z ∩ (Y ∪ U) = ∅. Let Ass′_{S}(d) be defined as in Figure 1. Then, for each d ∈ DC, Ass′_{S}(d) is an invariant of S at d. Henceforth, let aff-indep denote

Ass′_{S}(d) = \{ \begin{matrix}⋁_{t∈L(d)}(gu(t) ∧ aff(t)) & ; & if d ≠ d_{0} and Z ∩ (Y ∪ U) = ∅ \\ I ∨ ⋁_{t∈L(d)}(gu(t) ∧ aff(t)) & ; & if d = d_{0} and Z ∩ (Y ∪ U) = ∅ \\ ⋁_{t∈L(d)} aff(t) & ; & if d ≠ d_{0}, Z ∩ U = ∅ and Z ∩ Y ≠ ∅ \\ I ∨ ⋁_{t∈L(d)} aff(t) & ; & if d = d_{0}, Z ∩ U = ∅ and Z ∩ Y ≠ ∅ \\ ⋁_{t∈L(d)} gu(t) & ; & if d ≠ d_{0}, Z ∩ Y = ∅ and Z ∩ U ≠ ∅ \\ I ∨ ⋁_{t∈L(d)} gu(t) & ; & if d = d_{0}, Z ∩ Y = ∅ and Z ∩ U ≠ ∅ \\ true & ; & otherwise \end{matrix}

Fig. 1. Definition of Ass′_{S}(d)

the function that for a given transition system S returns as result the predicate ⋀_{d∈D} pc = d ⇒ Ass′_{S}(d). Generalized Reaffirmed Invariance with Cycles Consider the situation described in Figure 2. Then, function aff-indep yields the predicate x = 2 ∨ y = 1 as invariant at d. It is easy to see, however, that the stronger predicate x = 2 is also invariant at d. We develop a technique that extends the previous one and covers situations similar to that of Figure 2.

[figure: d_{0}; d′; d; x := 2; y := 1]

Fig. 2. Generalized Reaffirmed Invariance

A path from d to d′ in S is a sequence d_{1}, t_{1}, ⋯, t_{n−1}, d_{n} with n ≥ 2, d_{1} = d, and d_{n} = d. We say that a path d_{1}, t_{1}, ⋯, t_{n−1}, d_{n} from d to d′ goes through d′′, if d_{i} = d′′, for some i ∈ {1, ⋯, n}.

Definition 5. Given a transition system S, a control location d of S, and a set α of control locations of S with d ∈ α. We say that α is guarded by d, if the following conditions are satisfied:

– The initial control location of S is not in α or it is d.

– For every transition t ∈ L(α) \ {d}, sour(t) ∈ α.

– Each path from d to d′ ∈ α goes only through control locations in α.

Let Tr(S, α, d) denote the set L(α) \ {t | t ∈ L(d), sour(t) ∉ α}.

Example 1. Consider the system S given in Figure 3, where d_{0} is the initial control location. Then, α_{1} = {d_{1}, d_{2}, d_{3}, d_{4}, d_{5}} and α_{2} = {d_{1}, d_{4}, d_{5}} are guarded by d_{1}, while α_{3} = {d_{1}, d_{2}, d_{4}, d_{5}} and α_{4} = {d_{1}, d_{2}, d_{3}} are not because the second respectively third condition are violated. We have Tr(S, α_{1}, d_{1}) = {t_{1}, t_{2}, t_{3}, t_{4}, t_{5}, t_{6}} and Tr(S, α_{2}, d_{1}) = {t_{4}, t_{5}, t_{6}}.

Definition 6. Given a transition system S and d ∈ DC. We say that d is safe with respect to a set V of variables and a set α of control locations, if α is guarded by d and for every t ∈ Tr(S, α, d), t does not affect any variable in V.

[figure: d_{0}; t_{0}; d_{1}; t_{1}; d_{2}; d_{3}; t_{2}; t_{3}; t_{4}; d_{4}; d_{5}; t_{5}; t_{6}] Fig. 3.

Then we have the following lemma.

Lemma 7. Consider a transition system S, a control location d, a set α of control locations, and a set V of variables such that d is safe w.r.t. V and α. Let S′ denote the transition system obtained from S by removing the transitions in Tr(S, α, d). For every predicate Q with free variables V, if Q is an invariant of S′ at d, then Q is an invariant of S at every d′ ∈ α. The lemma above suggests a procedure to derive an invariant aff-cyc(S) from the description of the transition system S: For each d ∈ DC, determine a maximal set α of control locations for which d is safe with respect to the variables affected by transitions in {t | t ∈ L(d), sour(t) ∉ α}; in case d is the initial control location, we have to check also w.r.t. the free variables of I. If this is the case, record Ass′_{S′}(d), where S′ is as above, as an invariant of S at d′ for each d′ ∈ α, otherwise, record Ass′_{S}(d) as an invariant of S at d.

Remark. 1. A possible variant of the algorithm aff-cyc concerns the case where the initial control location is considered. Instead of requiring that d is safe w.r.t. the free variables of I, we hide those which could be affected by some transition in Tr(S, α, d) by existential quantification.

2. Clearly, determining the maximal set α which is guarded by d and then checking whether d is safe w.r.t. this set and the variables affected by transitions in {t | t ∈ L(d), sour(t) ∉ α} does not always allow to derive the strongest possible predicate. One can, however, have a procedure which depends on some given set V of variables and which computes the maximal set α such that d is safe w.r.t. V and α.

3. Until now we considered a single transition system S and aff-cyc has been formulated for this case. When n transition systems S_{1} ∥ ⋯ ∥ S_{n} in parallel are considered, we have to strengthen the notion of d being safe w.r.t. a set V of variables and a set α of control locations; and require that all variables in V are only written by the system S_{i} to which d belongs. Henceforth, whenever we refer to aff-cyc when a parallel program is considered, we mean the algorithm obtained by strengthening this notion and taking into account the variation suggested in 1.

Next, we present a technique that allows to propagate predicates that have been proved to be invariant at some control points of the system, i.e. for some value of pc. We first start with the basic idea. Propagation without cycles Given a transition system S, a predicate Q with V as free variables and a transition t of S, we say that transition t does not affect Q, if Z ∩ V = ∅, where Z are the variables affected by t.

Consider a transition system S and a control location d ∈ DC which is not the initial one. Let {d_{1}, ⋯, d_{n}} = sour(L(d)) and assume that, for each i ∈ {1, ⋯, n}, Q_{i}(V_{i}) is an invariant of S at d_{i}. If for each t ∈ L(d) and i ∈ {1, ⋯, n}, with sour(t) = d_{i}, t does not affect V_{i}, then ⋁_{i=1}^{n} Q(V_{i}) is an invariant at d. For the case where d is the initial control location, ⋁_{i=1}^{n} Q(V_{i}) ∨ I, where I is the initial predicate, is an invariant at d. The correctness of this observation is guaranteed by the following lemma.

Lemma 8. Consider a transition system S and a predicate P that is an invariant of S. Let d ∈ DC be a control location of S with L(d) = {t_{1}, ⋯, t_{m}} and d_{i} = sour(t_{i}). Let also Q_{1}, ⋯, Q_{m} be predicates such that P ∧ pc = d_{i} implies Q_{i}, with i = 1, ⋯, m. If d is not the initial control location of S, then the predicate P ∧ (l = d ⇒ ⋁_{i=1}^{m} post[→_{t_{i}}](Q_{i})) is an invariant of S, otherwise P ∧ (l = d ⇒ (⋁_{i=1}^{m} post[→_{t_{i}}](Q_{i}) ∨ I)) is an invariant of S.

Note that in case that transition t does not affect Q, we have post[→_{t}](Q) ⇒ Q, and therefore, the correctness of our technique is implied by the lemma above and the fact that if P′ is an invariant of S and P′ implies Q′, then Q′ is also an invariant of S.

The implementation of this technique is a function, denoted propg, that takes as input a transition system S and a predicate P of the form ⋀_{d∈DC} pc = d ⇒ Q_{d}(V′_{d}). Then, computes for each control location d, the set of variables affected by any transition in L(d). Let V_{d} denote the intersection of this set with V′_{d}. As result, this function yields, for each control location d, as a local invariant at d

the predicate Q_{d}(V′_{d}) ∧ ∃V_{d} · ⋁_{d′∈L(d)} Q_{d′}(V′_{d′}) .

Propagation with cycles Consider now the situation described in Figure 4. An application of the simple propagation technique does not allow to strengthen the predicate ⋀_{i=1}^{m} pc = d_{i} ⇒ x = i. For, we would add as a conjunct the predicate pc = d ⇒ true ∨ ⋁_{i=1}^{m} x = i, which is equivalent to true. Yet, it is clear that ⋁_{i=1}^{m} x = i is an invariant at d. We develop the next technique which captures similar situations.

[figure: x = 1; d_{1}; x = m; d_{m}; d; y := e; y := e_{1}; y := e_{m}; ⋮]

Fig. 4. Propagation with cycles

Consider a control location d and a set α of control locations which is guarded by d. Let {d_{1}, ⋯, d_{m}} = sour(L(d)) \ α. Then, if for each i = 1, ⋯, m, Q_{i}(V_{i}) is an invariant of S at d_{i} and if d is safe w.r.t. ⋃_{i=1}^{m} V_{i} and α, we can conclude by Lemma 7 and Lemma 8 that ⋁_{i=1}^{m} Q_{i}(V_{i}) is an invariant at each d′ ∈ α.

Mixing generalized reaffirmed invariance and propagation Until now we considered propagation and reaffirmed invariance separately. Whereas propagation assumes a given invariant P and propagates local invariants from control locations to others, reaffirmed invariance does not assume such a predicate. We now present a technique that combines propagation and reaffirmed invariance.

Consider a transition system S and an invariant P of S. Let d be a control location of S such that {t_{1}, ⋯ t_{m}} = L(d) and d_{i} = sour(t_{i}), for i = 1, ⋯, m. Suppose that for each i = 1, ⋯, m, P ∧ pc = d_{i} implies Q_{i}(V_{i}). If, for each transition t_{i} and each j with d_{j} = sour(t_{i}), Q_{i}(V_{i}) implies e(U_{i}) = C_{i} and Z_{i} ∩ V_{j} = ∅, where Z_{i}′ = e(U_{i}) is aff(t_{i}) and C is a list of constants, then we can conclude that ⋁_{i=1}^{m}(Q_{i}(V_{i}) ∧ Z_{i} = C_{i}) is invariant at d. Correctness of this observation is again a consequence of Lemma 8 and Lemma 8.

Refined Strengthening Suppose we are given a proposed invariant P for transition system S with transitions T. Suppose also that the proof of P ⇒ p̃re[→_{t}](P) fails for t_{1}, ⋯, t_{m}. The method of strengthening invariants (e.g. [15]) proposes to try as next invariant P_{1} = P ∧ ⋀_{i=1}^{m} p̃re[→_{t_{i}}](P). Thus, one has to try to prove for each transition t the implication P ∧ Q ⇒ p̃re[→_{t}](P ∧ Q), where Q = ⋀_{i=1}^{m} p̃re[→_{t_{i}}](P). The main drawback of this method is that, in general, each strengthening step increases the size of the considered invariant which in some cases leads to unreadable predicates.

We propose a variant of this method that is theoretically equivalent, i.e. it leads to logically equivalent verification conditions, but which allows to reduce the number of applications of p̃re and to save redoing proofs.

Suppose that the attempt of proving ∀t ∈ T · (P ⇒ p̃re[→_{t}](P)) fails for the transitions t_{1}, ⋯, t_{m}, and that one gets subgoals Q_{1}, ⋯, Q_{m}, which are logically equivalent to P ⇒ p̃re[→_{t_{i}}](P), i = 1, ⋯, m. We propose to take in the next step the predicate P′_{1} = P ∧⋀_{i=1}^{m} Q_{i} instead of P_{1}. The next lemma implies soundness of our method but also proves that if P_{1} is inductive, then also P′_{1}.

Lemma 9. Let P_{1} = P ∧⋀_{i=1}^{m} p̃re[→_{t_{i}}](P), Q_{i} be equivalent to P ⇒ p̃re[→_{t_{i}}](P), and let P′_{1} = P ∧ ⋀_{i=1}^{m} Q_{i}. Then, P_{1} and P′_{1} are equivalent.

It is worth to note that soundness of our method does not depend on the fact that Q_{i} is equivalent to P ⇒ p̃re[→_{t_{i}}](P) but it suffices, if it is stronger.

To see that our method indeed avoids the blow-up of the considered predicates which is due to the repeated application of the predicate transformer p̃re, let us look at the predicates to be considered at step i when each of the strengthening and refined strengthening methods are applied in turn. In case of the strengthening method, one has to consider at step i the predicate P_{i} = P_{0} ∧ p̃re(P_{0}) ∧ ⋯ p̃re^{i}(P_{i−1}) and to prove P_{i} ⇒ p̃re(P_{i}). In case of the refined strengthening method, however, one has to consider the predicate Q_{i} which is obtained as a subgoal in step i, and then, to prove Q_{0} ∧ ⋯ ∧ Q_{i} ⇒ p̃re(Q_{i}). Thus, in the refined strengthening method, at each step p̃re has to be applied only once. Another advantage of this method is that Q_{i} is usually of the form pc = d ⇒ Q which can be explained by the fact that Q_{i} is the predicate that is obtained when the proof of Q_{0} ∧⋯∧Q_{i−1} ⇒ p̃re(Q_{i−1}) for some fixed transition with pc = d as part of the enabling condition has been attempted. Now, when a predicate Q of the form pc = d ⇒ Q′ is considered in order to prove that Q is preserved by all transitions, it suffices to consider only those in L(d).

Combining Invariants Consider a network S = S_{1} ∥ ⋯ ∥ S_{n} of transition systems. Given a predicate P, in order to prove that P is an invariant of S, one can calculate the product S_{1} ⨂ ⋯ ⨂ S_{n} and then prove that P is an invariant of the resulting sequential transition system. This method is, however, not applicable for large transition systems because of the big size of the obtained system. Indeed, the resulting transition system mainly codes all possible interleaving of the transition steps in the network S. In this section, we present techniques we use to prove invariance properties of networks without calculating the product. These techniques have been successfully applied to many mutual exclusion algorithms, e.g. the Bakery mutual exclusion algorithm [12, 15] in three different versions and Szymanski’s mutual exclusion algorithm [18, 19] both parameterized and for two processes.

Definition 10. Given a transition system S, a predicate P is called historyindependent assertion at d ∈ DC, if post[t](true) ⊆ [[P]] holds for each t ∈ L(d), and moreover, if d is the initial control location of S, then Init implies P.

An history-independent assertion at d is true whenever computation reaches d independently on how this happens, in particular it does not dependent on the state in which the transition is taken.

Consider transition systems S_{1} and S_{2} with S_{i} = ⟨X_{i}, pc_{i} : DC_{i}, T_{i}, I_{i} ∧ pc_{i} = d_{i,0}⟩, for i = 1, 2. Moreover, consider predicates Q_{i}, for i = 1, 2, and (d_{1}, d_{2}) ∈ DC_{1} × DC_{2}. Assume we know that Q_{i} is an history-independent assertion at d_{i}. Then, we can conclude that Q_{1} ∨ Q_{2} is an invariant of S_{1} ∥ S_{2} at (d_{1}, d_{2}). This leads to the following heuristic formulated in the next lemma.

Lemma 11. Let S_{i} = ⟨X_{i}, pc_{i} : DC_{i}, T_{i}, I_{i} ∧pc_{i} = d_{i,0}⟩, for i = 1, 2, be transition systems and let Q_{i} be predicates. Then, for each (d_{1}, d_{2}) ∈ DC_{1} × DC_{2} such that Q_{i} is an history-independent assertion of S_{i} at d_{i}, for i = 1, 2, the predicate Q_{1} ∨ Q_{2} is an invariant of S_{1} ∥ S_{2} at (d_{1}, d_{2}).

If the predicates Q_{1} and Q_{2} constraint only variables which are affected only in S_{1}, respectively, S_{2}, then we can even conclude that the stronger predicate Q_{1} ∧ Q_{2} is an invariant at (d_{1}, d_{2}).

The implementation of both observations above is realized by a single function comp which takes as arguments the transition systems S_{1} and S_{2} as well as two predicates P_{1} and P_{2} for S_{1} and S_{2}, respectively, which are of the form ⋀_{d_{j}∈DC_{i}} pc = d_{j} ⇒ P_{i}(d_{j}), i = 1, 2. The result of the application of this function

is a predicate of the form ⋀_{d∈DC} pc = d ⇒ Q(d), where DC = DC_{1} × DC_{2} and for

d = (d_{1}, d_{2}), Q(d) is defined in Figure 3.

Remark. It is worth to note that each invariant Q obtained by applying the function aff-indep is history-independent.

In a concrete implementation, the predicate obtained by an application of the function comp, can be encoded by adding to each local invariant P_{i}(d_{i}) at d_{i} two bits. The first one encodes whether P_{i}(d_{i}) is history-independent and the second whether it refers to a variable affected in S_{j} with j ≠ i.

Q(d) = \{ \begin{matrix}P_{1}(d_{1}) ∨ P_{2}(d_{2}) & ; & if for i = 1, 2, P_{i} is an history-independent assertion atd_{i} \\ & & and one of the predicates P_{1} or P_{2} refers to a variable \\ & & affected in S_{2} respectively S_{1} \\ P_{1}(d_{1}) ∧ P_{2}(d_{2}) & ; & if for i = 1, 2, P_{i} is an history-independent assertion at d_{i} \\ & & and predicate P_{1} respec. P_{2} does not refer to any variable \\ & & affected in S_{2} respec. S_{1} \\ true & ; & otherwise \end{matrix}

Fig. 5. Definition of comp

The next lemma shows how given d′_{i} ∈ DC_{i} and a predicate Q that is historyindependent at d′_{i}, we can deduce a predicate Q′ which is also history-independent at d′_{i} and which does not refer to variables affected in S_{j} with j ≠ i.

Lemma 12. Let S_{1} and S_{2} be transition systems and let d_{1} ∈ DC_{1} (resp. d_{2} ∈ DC_{2}) be a control location of S_{1} (resp. S_{2}). If Q is a history-independent assertion at d and Y are the variables occurring in Q which are affected in S_{2} (resp, S_{1}), then ∃Y · Q is a history-independent assertion at d.

Clearly, the predicate ∃Y : D · Q does not refer to variables affected in S_{j}. Let abst be a function that takes as arguments two transition systems S_{1} and S_{2} and a predicate P for S_{1}, and returns a predicate Q for S_{1} such that Q is obtained from P by applying the observation above.

Next we present the tactic we apply to synthesize an invariant from a given network S_{1} ∥ S_{2}. This is presented by an algorithm written in pseudo-code and which uses the heuristics presented above.

Input: S_{1} ∥ S_{2}

Output: An invariant

1. P_{i} := aff-indep(S_{i}), for i = 1, 2

2. P := comp(S_{1}, S_{2}, P_{1}, P_{2})

3. Q_{1} := abst(S_{1}, S_{2}, P_{1}), Q_{2} := abst(S_{2}, S_{1}, P_{2})

4. Q_{i} := Q_{i} ∧ propg(S_{i}, Q_{i}), for i = 1, 2

5. return P ∧ Q_{1} ∧ Q_{2}

4 Example

The example we consider is the Bakery mutual exclusion algorithm [12, 15]. Two processes are competing to enter their respective critical sections represented by location 4. Thus, the invariant we are going to prove is given by the predicate INV = ¬(pc_{1} = 4 ∧ pc_{2} = 4).

It can easily be checked that this invariant is not inductive. Moreover, calculating the set of reachable states using the post operator does not terminate (no fix-point can be reached in a finite number of steps). Calculating the weakest invariance property that is contained in INV does terminate after 8 steps (cf. [14]). We can automatically generate by our techniques an invariant that is inductive and that allows to prove that INV is indeed an invariant.

Transition system S_{1}  | Transition system S_{2}
pc_{1} = 1 ⟶ pc′_{1} = 2  | pc_{2} = 1 ⟶ pc′_{2} = 2
pc_{1} = 2 ⟶ y′_{1} = y_{2} + 1, pc′_{1} = 3  | pc_{2} = 2 ⟶ y′_{2} = y_{1} + 1, pc′_{2} = 3
pc_{1} = 3 ∧ (y_{2} = 0 ∨ y_{1} ≤ y_{2}) → pc′_{1} = 4 | pc_{2} = 3 ∧ (y_{1} = 0 ∨ y_{2} < y_{1}) → pc′_{2} = 4
pc_{1} = 4 ⟶ pc′_{1} = 5  | pc_{2} = 4 ⟶ pc′_{2} = 5
pc_{1} = 5 ⟶ y′_{1} = 0, pc′_{1} = 1  | pc_{2} = 5 ⟶ y′_{2} = 0, pc′_{2} = 1
Init = (y_{1} = y_{2} = 0 ∧ pc_{1} = pc_{2} = 1)

Applying generalized reaffirmed invariance without cycles for S_{1} (resp. S_{2}) yields the predicate P_{1} (resp. P_{2}) with:

\begin{aligned}P_{1} = & (pc_{1} = 1 ⇒ y_{1} = 0 ∨ y_{1} = 0 ∧ y_{2} = 0) ∧ (pc_{1} = 3 ⇒ y_{1} = y_{2} + 1) ∧ \\ & (pc_{1} = 4 ⇒ y_{2} = 0 ∨ y_{1} ≤ y_{2}) \end{aligned}

\begin{aligned}P_{2} = & (pc_{2} = 1 ⇒ y_{2} = 0 ∨ y_{1} = 0 ∧ y_{2} = 0) ∧ (pc_{2} = 3 ⇒ y_{2} = y_{1} + 1)∧ \\ & (pc_{2} = 4 ⇒ y_{1} = 0 ∨ y_{2} < y_{1}) \end{aligned}

Combining the predicates P_{1} and P_{2} according to function comp results in a predicate equivalent to

P = (pc = (1, 1) ⇒ y_{1} = 0 ∨ y_{2} = 0) ∧ (pc = (1, 3) ⇒ y_{1} = 0 ∨ y_{2} = y_{1} + 1) ∧
(pc = (1, 4) ⇒ y_{1} = 0 ∨ y_{2} < y_{1}) ∧ (pc(3, 1) ⇒ y_{1} = y_{2} + 1 ∨ y_{2} = 0) ∧

(pc = (3, 3) ⇒ y_{1} = y_{2} + 1 ∨ y_{2} = y_{1} + 1) ∧ (pc = (3, 4) ⇒ y_{1} = 0 ∨ y_{2} < y_{1}) ∧

(pc = (4, 1) ⇒ y_{2} = 0 ∨ y_{1} ≤ y_{2}) ∧ (pc = (4, 3) ⇒ y_{2} = 0 ∨ y_{2} < y_{1})

In the sequel, we write pc_{1} = d_{1} ∧ pc_{2} = d_{2} for pc = (d_{1}, d_{2}). Next, we apply the abstraction function abst on P_{1} and P_{2} to obtain:

\begin{matrix}Q_{1} = & (pc_{1} = 1 ⇒ y_{1} = 0) ∧ (pc_{1} = 3 ⇒ y_{1} ≥ 1) \\ Q_{2} = & (pc_{2} = 1 ⇒ y_{2} = 0) ∧ (pc_{2} = 3 ⇒ y_{2} ≥ 1) \end{matrix}

Then, we apply our propagation technique without cycles. It can easily be checked that we can propagate from control location 1 to 2, from 3 to 4, and from 4 to 5, which yields the following predicates:

\begin{matrix}Q′_{1} = & (pc_{1} = 1 ∨ pc_{1} = 2 ⇒ y_{1} = 0) ∧ (pc_{1} = 3 ∨ pc_{1} = 4 ∨ pc_{1} = 5 ⇒ y_{1} ≥ 1) \\ Q′_{2} = & (pc_{2} = 1 ∨ pc_{2} = 1 ⇒ y_{2} = 0) ∧ (pc_{2} = 3 ∨ pc_{2} = 4 ∨ pc_{2} = 5 ⇒ y_{2} ≥ 1) \end{matrix}

Then, we can show P ∧ Q′_{1} ∧ Q′_{2} ∧ INV ⇒ p̃re[→_{t}](INV), for each transition t of S_{1} ∥ S_{2}.

5 Discussion and Future Work

This paper provides a set of techniques for the automatic generation of auxiliary predicates to prove invariants of programs. The use of these heuristics for the verification of various mutual exclusion algorithms shows that they are promising. They have been applied to different versions of the Bakery, Dekker, Peterson, and Szymanski algorithms (see [15] for a recent presentation of many of these algorithms and for references). Concerning Szymanski’s mutual exclusion algorithm, we verified the parameterized as well as the unparameterized case. We intend to combine our techniques with others as abstract interpretation [5] to discover relationships between program variables that can be used to derive invariants and to investigate heuristics and strategies for the decomposition of large programs. Acknowledgements We thank J. Sifakis who continuously encouraged and supported this work. Many interesting discussions with S. Graf and A. Pnueli helped clarifying and fixing our ideas. We also thank the anonymous referees for judecious comments.

References

1. K.R. Apt. Ten years of Hoare’s logic : a survey, part I. ACM Trans. on Prog. Lang. and Sys., 3(2):431–483, 1981.

2. N. Bjøner, A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. In U. Montanari, editor, 1st Int. Conf. on Principles and Practice of Constraint Programming, 1995.

3. M. Caplain. Finding invariant assertions for proving programs. In Proc. Int. Conf. on Reliable Software, Los Angeles, CA, 1975.

4. E.M. Clarke, E.A. Emerson, and E. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In POPL’83. ACM, 1983.

5. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM symp. of Prog. Lang., pages 238–252. ACM Press, 1977.

6. E. W. Dijkstra. Guarded commands, nondeterminacy, and formal derivation. Comm. ACM, 18(8):453–457, 1975.

7. B. Elspas. The semiautomatic generation of inductive assertions for proving program correctness. Research report, SRI, Menlo Park, CA, 1974.

8. R. W. Floyd. Assigning meanings to programs. In In. Proc. Symp. on Appl. Math. 19, pages 19–32. American Mathematical Society, 1967.

9. S. M. German and B. Wegbreit. A synthesizer of inductive assertions. IEEE Trans. On Software Engineering, 1:68–75, March 1975.

10. S. Graf and H. Saidi. Verifying invariants using theorem proving. In In this volume, 1996.

11. S. Katz and Z. Manna. A heuristic approach to program verification. In Proc. 3rd Int. Joint Conf. on Artificial Intelligence, Stanford,CA, 1976.

12. L. Lamport. A new solution of Dijkstra’s concurrent programming problem. Comm. ACM, 17(8):453–455, 1974.

13. O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In POPL, pages 97–107, 1985.

14. Z. Manna, A. Anuchitanukul, N. Bjøner, A. Browne, E. Chang, M. Colon, L. De Alfaro, H. Devarajan, H. Sipma, and T. Uribe. STeP : The Stanford Temporal Prover. Technical report, Stanford Univ., Stanford, CA, 1995.

15. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.

16. S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for faulttolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 1995.

17. J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. 5th Int. Sym. on Programming, volume 137 of Lecture Notes in Computer Science, pages 337–351. Springer-Verlag, 1982.

18. B. K. Szymanski. A simple solution to Lamport’s concurrent programming problem verification. In Proc. Intern. Conf. on Supercomputing Sys., pages 621–626, 1988.

19. B. K. Szymanski and J. M. Vidal. Automatic verfication of a class of symmetric parallel programs. In Proc. 13th IFIP World Computer Congress, 1994.

20. M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS’86. IEEE, 1986.

This article was processed using the L^{A}TEX macro package with LLNCS style